Apply unknownprop_566d903739470afda40d64020ac73735d543ec3209342e2b92a42fa9f217751d with
λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))),
λ x0 : ι → ι . λ x1 . 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_b9e6d5b35571f03f64e8d464e3aeeb947c17781fcebbb508bd1e4f61ea58ad5e.
The subproof is completed by applying unknownprop_b69aeea3b10b846ee5e419c1b471f03ef85ead2b77c13f4aa8b04c94af6c6775.