Let x0 of type ι be given.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
4a7ef...
Apply H0 with
λ x1 x2 . prim1 4a7ef.. x1.
The subproof is completed by applying unknownprop_f2280590a4843dd3047de5e5151d043be723c7f73a981e4edcbfbfe0904566e7 with x0.