Let α be given.

Assume Ha: ordinal α.

Let β be given.

Assume Hb: ordinal β.

Let γ be given.

Assume Hc: γ ∈ β.

We prove the intermediate claim La: SNo α.

An exact proof term for the current goal is ordinal_SNo α Ha.

We prove the intermediate claim Lb: SNo β.

An exact proof term for the current goal is ordinal_SNo β Hb.

We prove the intermediate claim Lc: ordinal γ.

An exact proof term for the current goal is ordinal_Hered β Hb γ Hc.

We prove the intermediate claim Lc2: SNo γ.

An exact proof term for the current goal is ordinal_SNo γ Lc.

rewrite the current goal using add_SNo_com α γ La Lc2 (from left to right).

rewrite the current goal using add_SNo_com α β La Lb (from left to right).

An exact proof term for the current goal is add_SNo_ordinal_InL β Hb α Ha γ Hc.

∎