proposition: Lemma freeVarSubAllTerms2 (a : nat) (ts : fol.Terms L a) (m : nat -> fol.Term L) (v n : nat): In n (freeVarTs ts) -> In v (freeVarT (m n)) -> In v (freeVarTs (subAllTerms a ts m)).
proof: Proof. intros H H0; induction ts as [| n0 t ts Hrects]. - apply H. - simpl; unfold freeVarTs; fold (freeVarT (subAllTerm t m)); fold (freeVarTs (subAllTerms n0 ts m)). apply in_or_app. unfold freeVarTs in H; fold (freeVarT t) in H; fold (freeVarTs ts) in H. induction (in_app_or _ _ _ H) as [H1 | H1]. + left; eapply freeVarSubAllTerm2. * apply H1. * assumption. + auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)