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