Apply ordinal_In_SNoLt 2 ordinal_2 1 to the current goal.

We will prove 1 ∈ 2.

An exact proof term for the current goal is In_1_2.

∎