Let p be given.
Assume H1: ∀n, nat_p n → (∀m ∈ n, p m) → p n.
We prove the intermediate claim L1: ∀n : set, nat_p n → ∀m ∈ n, p m.
Apply nat_ind to the current goal.
We will prove ∀m ∈ 0, p m.
Let m be given.
Assume Hm: m ∈ 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀m ∈ n, p m.
We will prove ∀m ∈ ordsucc n, p m.
Let m be given.
Assume Hm: m ∈ ordsucc n.
We will prove p m.
Apply (ordsuccE n m Hm) to the current goal.
Assume H2: m ∈ n.
An exact proof term for the current goal is (IHn m H2).
Assume H2: m = n.
We will prove p m.
rewrite the current goal using H2 (from left to right).
We will prove p n.
An exact proof term for the current goal is (H1 n Hn IHn).
We will prove ∀n, nat_p n → p n.
An exact proof term for the current goal is (λn Hn ⇒ H1 n Hn (L1 n Hn)).
∎