proposition: Lemma freeVarMap1 (l : list nat) (m : nat -> fol.Term L) (v n : nat): In v (freeVarT (m n)) -> In n l -> In v (freeVarMap l m).
proof: Proof. intros H H0; induction l as [| a l Hrecl]. - elim H0. - induction H0 as [H0| H0]. + simpl; rewrite H0; auto with datatypes. + simpl; auto with datatypes. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)