Claim L1:
or (1 ∈ 0) (0 = 1)Apply H0 with
0,
0 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply ordinal_ordsucc with
0.
The subproof is completed by applying ordinal_Empty.
Assume H2: 1 ∈ 0.
Apply EmptyE with
1.
The subproof is completed by applying H2.
The subproof is completed by applying neq_0_ordsucc with 0.
Apply unknownprop_f2665e7d9d9aff04a54f0326c3182ba0030a187604c1d0b27e5a9bebd4051089 with
1 ∈ 0,
0 = 1,
False leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.