Let x0 of type ι be given.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
x0,
x0,
λ x1 . x1.
The subproof is completed by applying unknownprop_91304e970b361e41c03c780112a4270a3e7ddd88b2f71983e3ae704ef3ddb5ec with x0.