Let x0 of type ι be given.
Apply unknownprop_7f3377c88b4409d85225bd10726cc6caca85db3671a8e3d8d0e75f9aea9723e4 with
x0,
x0.
The subproof is completed by applying unknownprop_b88c7d2cc71b4f494bf94f485b6de710e53401c58179aa2c5662393601237d01 with
SNoLev x0,
λ x1 . In x1 x0.