Apply unknownprop_566d903739470afda40d64020ac73735d543ec3209342e2b92a42fa9f217751d with
λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))),
λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))) leaving 2 subgoals.
The subproof is completed by applying unknownprop_e8e6d5cd52803fa78978937f5cadf0b90ae1da5571c1821cbca428bd99b61202.
The subproof is completed by applying unknownprop_ed572293a6fa0ec02a803cad7d3df6b0e0146a679954f245b5255a74225de76b.