Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Apply ordinal_In_Or_Subq with 0, ordsucc x0, 0ordsucc x0 leaving 4 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply ordinal_ordsucc with x0.
The subproof is completed by applying H0.
Assume H1: 0ordsucc x0.
The subproof is completed by applying H1.
Assume H1: ordsucc x00.
Apply FalseE with 0ordsucc x0.
Apply EmptyE with x0.
Apply H1 with x0.
The subproof is completed by applying ordsuccI2 with x0.