We will prove 2 ∈ 3.

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

An exact proof term for the current goal is (ordsuccI2 2).

∎