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