proposition: Lemma PA2_sat_iff_empty_theory_sat (phi : @form PA2_funcs_signature PA2_preds_signature _) : PA2 ⊨ phi <-> (fun _ => False) ⊨ embed_PA2 phi.
proof: Proof. split. - intros H M rho HM. now apply PA2_model_valid_iff_model_valid. - intros H M. apply PA2_model_valid_iff_model_valid. intros M' rho. now apply (H M'). 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