Let x0 of type ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι → ι → ι be given.
Let x5 of type ι → ι → ο be given.
Assume H0:
∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ x4 x9 x10 = x8 x9 x10) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_8ea69fc9abac0355b105f07aa76ed34b3962fcf544d9757d1d9d05aa9d0cad83 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
2b2e3.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_9b67ca9ab1646382899bbdc59f47517de76380f07be13a5ce2de56c82d4796e9 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_1800ba7fa99d61c31829fa17fb98b2c724b98156c3096d47aa78e26b0544c68e with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_4296533c60aa73eebe625d72d0577a7e8b212c89496259f10b26dbb5c0255a76 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_c26ef7bf18140bad8d6953993defcebda527e5707dd4d63400179c3d1438050f with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x5 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x5 x6 x7.