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.
Assume H0:
∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x4 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4.
Apply unknownprop_36751e118df5c1b80ee289bfa85a0d6bea79da8ecbc4a6eae2f963f2b4d745c1 with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_148aab2e21bf4a2a0378620f413f6845c1c28ea43c2cda3058a8bdf8e236efe0 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_01ea101418f5daaf86be503b2a30dd4068502035cc9e9cf32078e9c4691abbaf with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_86854eea85b744d4bb31fb503cfb71e1d637fa5fbb6152b580f507236aa74287 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x4 x5 x6) x7 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 x5 x6.