Let x0 of type ι → (ι → ι → ο) → ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ο be given.
Assume H0:
∀ x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2.
Apply unknownprop_97f8046614ea7148c1fa23ec1426d82a984f022d6441770c46d9508e4193899d with
x1,
x2,
λ x3 x4 . x0 x3 (2b2e3.. (f482f.. (35983.. x1 x2) (4ae4a.. 4a7ef..))) = x0 x1 x2.
Apply H0 with
2b2e3.. (f482f.. (35983.. x1 x2) (4ae4a.. 4a7ef..)).
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_86d039171608909af3061792cdafdca234dab72c05fe9399d5fd5de804007d06 with
x1,
x2,
x3,
x4,
λ x5 x6 : ο . iff (x2 x3 x4) x5 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 x2 x3 x4.