Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 35983.. (f482f.. x1 4a7ef..) (2b2e3.. (f482f.. x1 (4ae4a.. 4a7ef..))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ο be given.
Apply unknownprop_97f8046614ea7148c1fa23ec1426d82a984f022d6441770c46d9508e4193899d with
x1,
x2,
λ x3 x4 . 35983.. x1 x2 = 35983.. x3 (2b2e3.. (f482f.. (35983.. x1 x2) (4ae4a.. 4a7ef..))).
Apply unknownprop_2887e84b91f46bec6af4cc04d802b5c7bffe733c595590b2f21daa1586245ec9 with
x1,
x2,
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.