An exact proof term for the current goal is form100_63_injCantor ω.