proposition: Lemma closedNN : forall v : nat, ~ In_freeVarSys LNN v NN.
proof: Proof. unfold not in |- *; intros v [x H]. destruct closedNN1 with v x; tauto. Qed.
imports: Coq(Arith Lia Ensembles List) hydras.Ackermann(folProp subAll folLogic3 Languages) hydras(Compat815 NewNotations)