proposition: Lemma PA2_closed : forall phi, PA2 phi -> closed phi.
proof: Proof. intros phi H. repeat destruct H as [<-|H]; cbv; firstorder. destruct (Nat.eq_dec ar 1) as [->|]. left; firstorder. right; firstorder. 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