Let x0 of type ι be given.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
0,
x0.
Let x1 of type ι be given.
Apply FalseE with
In x1 x0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x1.
The subproof is completed by applying H0.