proposition: Lemma PA2_Model_sat_PA2_form M : forall rho, (M, rho) ⊨ PA2 <-> (M, rho) ⊨ PA2_form.
proof: Proof. intros rho. split. - intros M_correct. repeat split; apply M_correct; repeat (try (left; reflexivity); try right). - intros H. intros phi H1. repeat destruct H1 as [<-|H1]; try apply H; try 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