proposition: Lemma closedPA : forall v : nat, ~ In_freeVarSys LNT v PA.
proof: Proof. intros v H; unfold In_freeVarSys in H. destruct H as [x H]; elim closedPA1 with v x; tauto. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)