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 ⟶ x3 x7 = x6 x7) ⟶ ∀ 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_ba194c2202ced89f547acbeed926c5ea6a29f7cca72cc88e80d18b7ebbb1e52d with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (e3162.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
e3162.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_325bcb5a256ab9329e80a14f794ea1b267596485f1c43f7b00c5997e3eb3ce72 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_1e75cd0b3307fe13c67a0c1db282e2e688fb42fc347d98829e01d0ac65464433 with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_7150e92e55bd9c994083b0e205f066c8c716fd2d7db929fded102f4c0566f20f 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.