(thm : (x : (P : ∗¹) →
                 (foo_ : (barfoo_ : A⇧¹) → (baz_ : A⇧¹) → P) →
                 P) →
            (y : (P : ∗¹) → (foo_ : (barfoo_ : A⇧¹) → (baz_ : A⇧¹) → P) → P) →
            ((P₁ : ∗¹) →
             (fooP₁ : ∗¹) →
             (P : (foo_ : P₁) → (bar_ : fooP₁) → ∗) →
             (_₁ : (foo_ : A⇧¹) → (bar_ : A⇧¹) → P₁) →
             (bar_₁ : (foo_ : A⇧¹) → (bar_ : A⇧¹) → fooP₁) →
             (baz_ : (foo_₁ : A⇧¹) →
                     (bazbar_₁ : A⇧¹) →
                     (foobar_ : A!!%² foo_₁ bazbar_₁) →
                     (fubar_₁ : A⇧¹) →
                     (qux_₁ : A⇧¹) →
                     (quux_ : A!!%² fubar_₁ qux_₁) →
                     P (_₁ foo_₁ fubar_₁) (bar_₁ bazbar_₁ qux_₁)) →
             P (x P₁ _₁) (y fooP₁ bar_₁)) →
            A!!%² (f⇧¹ x) (f⇧¹ y)) ×
     ∗₁


 (thm : (x : (P : ∗¹) → (A⇧¹ → A⇧¹ → P) → P) →
        (y : (P : ∗¹) → (A⇧¹ → A⇧¹ → P) → P) →
        ((P₁ : ∗¹) →
         (P₁ : ∗¹) →
         (P : P₁ → P₁ → ∗) →
         (_₁ : A⇧¹ → A⇧¹ → P₁) →
         (_₁ : A⇧¹ → A⇧¹ → P₁) →
         ((_₁ : A⇧¹) →
          (_₁ : A⇧¹) →
          A!!%² _₁ _₁ →
          (_₁ : A⇧¹) →
          (_₁ : A⇧¹) →
          A!!%² _₁ _₁ →
          P (_₁ _₁ _₁) (_₁ _₁ _₁)) →
         P (x P₁ _₁) (y P₁ _₁)) →
        A!!%² (f⇧¹ x) (f⇧¹ y)) ×
 ∗₁