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