Let x0 of type ι be given.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with
1,
x0,
λ x1 x2 . x2 = x0 leaving 3 subgoals.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_74e06c9344760e4cc873ef5c22b83470d591f1b41a22d02c74881e98d2f21e46 with x0.