Let x0 of type ι be given.
Assume H0:
∀ x1 . nIn x1 x0.
Apply unknownprop_73b312e5c0ced1987581817c61d2a6ab9e4c47a87f99557a6b2723117244e7d9 with
x0.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x0,
0.
Let x1 of type ι be given.
Apply FalseE with
In x1 0.
Apply notE with
In x1 x0 leaving 2 subgoals.
Apply unknownprop_9bccc16873f624a3c3c071d170820d76e64a5491b15f0c2f0287b0026ecb19b8 with
x1,
x0.
The subproof is completed by applying H0 with x1.
The subproof is completed by applying H1.