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