Apply unknownprop_f8517820c41e80abae5090668a4d7f9c31465f066f11281cc9990a74d008bfa1 with
λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))).
The subproof is completed by applying unknownprop_2169d21de601d42cf8c0876b332a1b9f60ec3afcda9c9b50cf06e052fa439595.