Let x0 of type ι → (ι → ι → ι) → CT2 ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι → ι be given.

Let x3 of type ι → ι → ι be given.

Assume H0: ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = x4 x5 x6) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = x5 x6 x7) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3.

Apply unknownprop_6b7bf5eb93cfba6ad06205d79f6c13a19f6adf11ee9d27c7f4dedac962dc7ebb with x1, x2, x3, λ x4 x5 . x0 x4 (e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..)))) = x0 x1 x2 x3.

Apply H0 with e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. 4a7ef..)), e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.

The subproof is completed by applying unknownprop_2150cc54b7f6d41dfc462a969c62a57722c34bb757034211e8fbb53f3d780b5b with x1, x2, x3.

The subproof is completed by applying unknownprop_946f379b9edd63a51735ac93ccc9c84b60365dbf0ae761e12e2463ecf24500a8 with x1, x2, x3.

■

Proofgold Proof