Let x be given.
Assume H1: x ∈ 2.
Apply ordsuccE 1 x H1 to the current goal.
Assume H2: x ∈ 1.
We prove the intermediate claim L1: x = 0.
An exact proof term for the current goal is (SingE 0 x (Subq_1_Sing0 x H2)).
We will prove x ∈ {0,1}.
rewrite the current goal using L1 (from left to right).
We will prove 0 ∈ {0,1}.
An exact proof term for the current goal is (UPairI1 0 1).
Assume H2: x = 1.
We will prove x ∈ {0,1}.
rewrite the current goal using H2 (from left to right).
We will prove 1 ∈ {0,1}.
An exact proof term for the current goal is (UPairI2 0 1).
∎