Search for blocks/addresses/...

Proofgold Proof

pf
Apply explicit_Nats_I with omega, 0, ordsucc leaving 5 subgoals.
The subproof is completed by applying unknownprop_87d981ec36961a0324ea5d0962fa0689e652a1a367082910c100751340d2d034.
The subproof is completed by applying omega_ordsucc.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
The subproof is completed by applying neq_ordsucc_0 with x0.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Let x1 of type ι be given.
Assume H1: x1 ∈ omega.
The subproof is completed by applying ordsucc_inj with x0, x1.
Let x0 of type ι → ο be given.
Assume H0: x0 0.
Assume H1: ∀ x1 . x0 x1 ⟶ x0 (ordsucc x1).
Let x1 of type ι be given.
Assume H2: x1 ∈ omega.
Claim L3: nat_p x1
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Apply L3 with x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■