Let L be given.
Assume H1.
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ 0, SNo y) ∧ (∀x ∈ L, ∀y ∈ 0, x < y).
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
Let y be given.
Assume Hy.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
∎