Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 64302.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (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_36751e118df5c1b80ee289bfa85a0d6bea79da8ecbc4a6eae2f963f2b4d745c1 with
x1,
x2,
x3,
x4,
λ x5 x6 . 64302.. x1 x2 x3 x4 = 64302.. x5 (e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_4e57c9886f1cc241309922302fa4cd05b7348f88d9f6d3449dd8cec635c35b9f with
x1,
x2,
e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
2b2e3.. (f482f.. (64302.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_148aab2e21bf4a2a0378620f413f6845c1c28ea43c2cda3058a8bdf8e236efe0 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_01ea101418f5daaf86be503b2a30dd4068502035cc9e9cf32078e9c4691abbaf with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_86854eea85b744d4bb31fb503cfb71e1d637fa5fbb6152b580f507236aa74287 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.