Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = a255b.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (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_d3b5acfee106d0e14fe58094c8e3c6f75e54c07e6481b9e36207e34ac8236fe5 with
x1,
x2,
x3,
x4,
λ x5 x6 . a255b.. x1 x2 x3 x4 = a255b.. x5 (e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_a30f2b493842bf3fcbc3d14b60dd37fb66336a1cdf7348034e2712053fdcc70a with
x1,
x2,
e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
f482f.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_8158cb53a6ed2c6ca20129fda5153cb308dc2ca6e90a584aa8a3f15eb6f871ea with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_6240d82b92741e6cbf5c66460b7082bc5753da2dd534074b46e0f43ee9335cf6 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_ea68f7a822834285aec4e0837699a1b95f35c6b4c76e31caccc8a9483647132a with x1, x2, x3, x4.