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