Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_inv_impred with λ x0 . x01or (x0 = 0) (x0 = 1) leaving 2 subgoals.
Assume H0: 01.
Apply orIL with 0 = 0, 0 = 1.
Let x0 of type ιιο be given.
Assume H1: x0 0 0.
The subproof is completed by applying H1.
Apply nat_inv_impred with λ x0 . ordsucc x01or (ordsucc x0 = 0) (ordsucc x0 = 1) leaving 2 subgoals.
Assume H0: 11.
Apply orIR with 1 = 0, 1 = 1.
set y0 to be 1
Let x1 of type ιιο be given.
Assume H1: x1 y0 y0.
The subproof is completed by applying H1.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ordsucc (ordsucc x0)1.
Apply FalseE with or (ordsucc (ordsucc x0) = 0) (ordsucc (ordsucc x0) = 1).
Apply In_irref with 1.
Apply H1 with 1.
Apply nat_ordsucc_in_ordsucc with ordsucc x0, 0 leaving 2 subgoals.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
Apply nat_0_in_ordsucc with x0.
The subproof is completed by applying H0.