Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
1,
Sing 0.
Let x0 of type ι be given.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
0,
x0,
In x0 (Sing 0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply FalseE with
In x0 (Sing 0).
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x0.
The subproof is completed by applying H1.
Assume H1: x0 = 0.
Apply H1 with
λ x1 x2 . In x2 (Sing 0).
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.