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 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (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_d577c0a69bb7f1b14a06ae9f0073ddf917ac85a7c69ec25a57d9b02c9e415a6d with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
2b2e3.. (f482f.. (d0dcf.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_e5e5f5ecc00890eeeb630ecdb18cefa221c83f9f4b437e4c138ec7b42f43d8f8 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_1f8c96ef329d385365e7d71b2532d34a0468c6739081f43a1ef46b84942419e3 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_39de345e81dba22a9be8c8991e3affd16e02f3c07866fd86c25e581f366541f0 with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x4 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 x4 x6 x7.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_7580d399474277d1cb39e1940f3b3c3f2a5a27129ea6ca66e732bd38b261f624 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.