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