Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = d89a7.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι be given.
Let x4 of type ι → ι → ο be given.
Apply unknownprop_ba194c2202ced89f547acbeed926c5ea6a29f7cca72cc88e80d18b7ebbb1e52d with
x1,
x2,
x3,
x4,
λ x5 x6 . d89a7.. x1 x2 x3 x4 = d89a7.. 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..))))).
Apply unknownprop_a3678084529c2077a3ba6f1d72d5e6bd60825e188cac406423f8dae3b8245e28 with
x1,
x2,
e3162.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
f482f.. (f482f.. (d89a7.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
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 H3.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x4 x5 x6.