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