Let p be given.
Assume H1: p 0.
Assume H2: ∀n, nat_p n → p n → p (ordsucc n).
We prove the intermediate claim L1: nat_p 0 ∧ p 0.
An exact proof term for the current goal is (andI (nat_p 0) (p 0) nat_0 H1).
We prove the intermediate claim L2: ∀n, nat_p n ∧ p n → nat_p (ordsucc n) ∧ p (ordsucc n).
Let n be given.
Assume H3: nat_p n ∧ p n.
Apply H3 to the current goal.
Assume H4: nat_p n.
Assume H5: p n.
Apply andI to the current goal.
We will prove nat_p (ordsucc n).
An exact proof term for the current goal is (nat_ordsucc n H4).
We will prove p (ordsucc n).
An exact proof term for the current goal is (H2 n H4 H5).
Let n be given.
Assume H3.
We prove the intermediate claim L3: nat_p n ∧ p n.
An exact proof term for the current goal is (H3 (λn ⇒ nat_p n ∧ p n) L1 L2).
An exact proof term for the current goal is (andER (nat_p n) (p n) L3).
∎