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