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 ⟶ x2 x6 = x5 x6) ⟶ ∀ 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_d0c6645deb4e4a12bb2d204629b8d932c7c9885969a4f1b009b789ca36525db2 with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (f482f.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
f482f.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_c2318c3dd65accea00dadff6d47933b4587e236518978f4378818dcb690ba2d2 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_707e1d17e1b6b9966d50c66b71426f61a607a2737b77d1bc99065964130a4803 with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_55e99137b7e579558f9997426e99fef7b5d8724c4376472bfc9654d8923b03ef 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.