Let p be given.

Assume H1: ∀α, ordinal α → (∀β ∈ α, p β) → p α.

Apply In_ind to the current goal.

Let α be given.

Assume IH: ∀β ∈ α, ordinal β → p β.

Assume H2: ordinal α.

We will prove p α.

Apply (H1 α H2) to the current goal.

Let β be given.

Assume H3: β ∈ α.

We will prove p β.

Apply (IH β H3) to the current goal.

We will prove ordinal β.

An exact proof term for the current goal is (ordinal_Hered α H2 β H3).

∎