Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 942b6.. (f482f.. x1 4a7ef..) (f482f.. (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_d0c6645deb4e4a12bb2d204629b8d932c7c9885969a4f1b009b789ca36525db2 with
x1,
x2,
x3,
x4,
λ x5 x6 . 942b6.. x1 x2 x3 x4 = 942b6.. 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..))))).
Apply unknownprop_3ad06d996aaf057ffff32f34bbac73f6ac9c0dd063bb04996d949e0d2e2c4915 with
x1,
x2,
f482f.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
f482f.. (f482f.. (942b6.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
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 H3.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x4 x5 x6.