Apply ordinal_In_SNoLt 2 ordinal_2 0 to the current goal.

We will prove 0 ∈ 2.

An exact proof term for the current goal is In_0_2.

∎