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