Let p be given.

Assume H1: ∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha.

Apply In_ind to the current goal.

Let alpha be given.

Assume IH: ∀beta ∈ alpha, ordinal beta → p beta.

Assume H2: ordinal alpha.

We will prove p alpha.

Apply (H1 alpha H2) to the current goal.

Let beta be given.

Assume H3: beta ∈ alpha.

We will prove p beta.

Apply (IH beta H3) to the current goal.

We will prove ordinal beta.

An exact proof term for the current goal is (ordinal_Hered alpha H2 beta H3).

∎