Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 7c612.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (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_8f65da788a93ff89d95bcf516abc29daa711f2c16faefefcaad5ba81f2e71786 with
x1,
x2,
x3,
x4,
λ x5 x6 . 7c612.. x1 x2 x3 x4 = 7c612.. x5 (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_ce65b626a980ba561f58bb8b39c0d11dacdb0f3848ef4b24fe353672c6edde75 with
x1,
x2,
e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_ff4535e6de7d81b5e64319b54276975d755c6038dfc6568b8eaad6de9e67f064 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_d91c9a6f9c15a2c6b9d2b80e56f063e4e1af105da6d9f1d5f7ab2c269bb9687a with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_d90cbda69461be2219583389e1055578190fbc4e0c943c03394d871429ab3a0a with x1, x2, x3, x4.