proposition: Lemma succ_inj' x y : iσ x i== iσ y -> x i== y.
proof: Proof. Proof using M_correct. apply (M_correct ax_succ_inj ltac:(easy) (empty_PA2_env _)). 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