Let x0 of type ι be given.
Apply unknownprop_cad282ef0fdd0498b9d72e39ef4bede1603c0487cbba81dcc7e691931f33d73a with
λ x1 . (λ x2 . 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1,
λ x1 x2 . 0ac37.. x0 x2 = x0.
The subproof is completed by applying unknownprop_ae9d3452c0cc3e7f2b12e2f8d218fbf318d4317bd92def71866cf2a9e1688e88 with x0.