proposition: Lemma to_domain_injective x x' : to_domain x = to_domain x' -> x = x'.
proof: Proof. Proof using M_correct. revert x'. induction x; destruct x'. - reflexivity. - now intros H%zero_succ. - intros H. symmetry in H. now apply zero_succ in H. - intros H%succ_inj. now rewrite (IHx x'). Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec