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