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