Let x0 of type ι be given.
Apply unknownprop_26d41f898c6d37a3ad32019e5b97968c60dddaf39b1307e24c8e605475b6f0d8 with
x0,
4a7ef..,
λ x1 x2 . x2 = x0.
The subproof is completed by applying unknownprop_fc17ae1257247ccbad94ae05ce6b26282126a44d809f22e0209b526a567506af with x0.