Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: x0 0.
Assume H1: ∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (add_CSNo x1 1).
Apply nat_ind with x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H2: nat_p x1.
Apply unknownprop_284dc111c6eb2bddb3c4d801652d8c8261bace09e41e64d83eb05adf646c0cc8 with x1, λ x2 x3 . x0 x1 ⟶ x0 x2 leaving 2 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H2.
Apply H1 with x1.
The subproof is completed by applying H2.
■