Let x0 of type ι be given.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
Inj1 x0 = 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
0.
Apply H0 with
λ x1 x2 . In 0 x1.
The subproof is completed by applying unknownprop_9998e40d8c081bcb0998eee5b18bc644807c64b4a7795024462a6db641b5bcc2 with x0.