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