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