Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_ind with λ x0 . ∀ x1 : ι → ι . (∀ x2 . x2x0nat_p (x1 x2))nat_p (Sigma_nat x0 x1) leaving 2 subgoals.
Let x0 of type ιι be given.
Assume H0: ∀ x1 . x10nat_p (x0 x1).
Apply unknownprop_2ab88bc3cb73bc8bbab980b6b6fd9d920b44f54ff9f8140f78b2a17b00566385 with x0, λ x1 x2 . nat_p x2.
The subproof is completed by applying nat_0.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 : ι → ι . (∀ x2 . x2x0nat_p (x1 x2))nat_p (Sigma_nat x0 x1).
Let x1 of type ιι be given.
Assume H2: ∀ x2 . x2ordsucc x0nat_p (x1 x2).
Apply unknownprop_32bc7778cd02b216f957f8c5e9693c4b58b7ca04a4ca47b5f3adb522add7dd35 with x0, x1, λ x2 x3 . nat_p x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_nat_p with Sigma_nat x0 x1, x1 x0 leaving 2 subgoals.
Apply H1 with x1.
Let x2 of type ι be given.
Assume H3: x2x0.
Apply H2 with x2.
Apply ordsuccI1 with x0, x2.
The subproof is completed by applying H3.
Apply H2 with x0.
The subproof is completed by applying ordsuccI2 with x0.