Let x0 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
Inj1 x0,
Sing 0.
Apply notE with
Inj1 x0 = 0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b4b5c3da03533cb8c3461d2e266a58e35501a748994747eb64c5640663ac3178 with x0.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
Inj1 x0.
The subproof is completed by applying H0.