Apply unknownprop_f8517820c41e80abae5090668a4d7f9c31465f066f11281cc9990a74d008bfa1 with
λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (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_5736f28d08664b9b7be676af8fe97d8bc5ccb918218c45c8c1dc935bd28d649e.