Apply ordinal_In_SNoLt 1 ordinal_1 0 to the current goal.

We will prove 0 ∈ 1.

An exact proof term for the current goal is In_0_1.

∎