proposition: Lemma closedNatToTerm : forall a v : nat, ~ In v (freeVarT (natToTerm a)).
proof: Proof. intros a v; induction a as [| a Hreca]. - cbn; auto. - simpl. now rewrite freeVarSucc. Qed.
imports: Coq(Arith Ensembles List) hydras.Ackermann(Languages folProof folProp folLogic3)