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