Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = b6bd3.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Apply unknownprop_6b7bf5eb93cfba6ad06205d79f6c13a19f6adf11ee9d27c7f4dedac962dc7ebb with
x1,
x2,
x3,
λ x4 x5 . b6bd3.. x1 x2 x3 = b6bd3.. x4 (e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..)))).
Apply unknownprop_59657b15fa50704c928efa7904aa80c89ba7986f22d94d96d5661e3140a3bbc7 with
x1,
x2,
e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (b6bd3.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
The subproof is completed by applying unknownprop_2150cc54b7f6d41dfc462a969c62a57722c34bb757034211e8fbb53f3d780b5b with x1, x2, x3.
The subproof is completed by applying unknownprop_946f379b9edd63a51735ac93ccc9c84b60365dbf0ae761e12e2463ecf24500a8 with x1, x2, x3.