Let x0 of type ι be given.
Apply unknownprop_73b312e5c0ced1987581817c61d2a6ab9e4c47a87f99557a6b2723117244e7d9 with
ap 0 x0.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
ap 0 x0,
0.
Let x1 of type ι be given.
Assume H0:
In x1 (ap 0 x0).
Claim L1:
In (lam 2 (λ x2 . If_i (x2 = 0) x0 x1)) 0Apply unknownprop_00442014bfaa26153a8a3beba70024a061e9854c1ec5733869154dfc3ef72462 with
0,
x0,
x1.
The subproof is completed by applying H0.
Apply FalseE with
In x1 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
lam 2 (λ x2 . If_i (x2 = 0) x0 x1).
The subproof is completed by applying L1.