An exact proof term for the current goal is (well_ordering_theorem_axiom A).