Let R be given.

Assume H1.

We will prove (∀x ∈ 0, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ 0, ∀y ∈ R, x < y).

Apply and3I to the current goal.

Let x be given.

Assume Hx.

We will prove False.

An exact proof term for the current goal is EmptyE x Hx.

An exact proof term for the current goal is H1.

Let x be given.

Assume Hx.

We will prove False.

An exact proof term for the current goal is EmptyE x Hx.

∎