Let x0 of type ι be given.
Apply unknownprop_e1da79ad2238fc685b3e4f7de09c0d965538bebf8c87c6f411479674dad88ab7 with
x0,
and (SNo (7cd66.. x0)) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) (7cd66.. x0)) leaving 2 subgoals.
The subproof is completed by applying H0.