Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 9b6e8.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x1 (4ae4a.. (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.
Let x5 of type ι be given.
Apply unknownprop_0663073412d695176e3e23ffbbbb5da2857252d5c0f47051c9f0c33ecb11f4b6 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . 9b6e8.. x1 x2 x3 x4 x5 = 9b6e8.. x6 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_a5be19faa2e80b8da858086292146d3f609318d0df557aec5c9ce5a6ab6b4ab0 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . 9b6e8.. x1 x2 x3 x4 x5 = 9b6e8.. x1 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_c1003d86b72ccf1c88f05bbb3160c1287244e653b755f6f0f8f6e6dea303f1e4 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . 9b6e8.. x1 x2 x3 x4 x5 = 9b6e8.. x1 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.
Apply unknownprop_7d246bf0e68f4796fefa8cfbc9dab886d0e6d737797c87a6ed01831e1a2add66 with
x1,
x2,
e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
x3,
f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a0d932da53985136bc4d111609d0ae5a2ed2e4f1789b9bd8811552fd687d1136 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_c64bca701150bd7d152f116af6a1108b34c2b6e6d2765f2dada41711a2cb9dfa with x1, x2, x3, x4, x5.