Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
0.
Apply H0 with
λ x0 x1 . In 0 x0.
The subproof is completed by applying unknownprop_8285cfa4fcfced8bf8f28f246aaeb081e0d4a211d67c239e326650337a8e69c8 with
99f52...