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