An exact proof term for the current goal is ordinal_SNoLev 0 ordinal_Empty.