Let x0 of type ι be given.
Apply unknownprop_af847e040e91b99dbf77a9d137cb8611c75d491ea2b42e1ae03082b87361b50c with
x0,
0,
λ x1 x2 . x2 = x0.
The subproof is completed by applying unknownprop_872273e895264b163d3a3b042c5d1abf262e26919401a643ccce2dcdcb6a14ef with x0.