proposition: Lemma std_model_correct : Standard_Model ⊨ PA2.
proof: Proof. intros phi H. repeat try destruct H as [<-|H]; hnf; cbn; try congruence. intros rho P H IH n. induction n; auto. easy. 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