Let x be given.

Assume H1: x ∈ 1.

We will prove x ∈ {0}.

Apply ordsuccE 0 x H1 to the current goal.

Assume H2: x ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE x H2).

Assume H2: x = 0.

rewrite the current goal using H2 (from left to right).

We will prove 0 ∈ {0}.

An exact proof term for the current goal is (SingI 0).

∎