proposition: Lemma freeVarSubAllTerms1 (n : nat) (ts : fol.Terms L n) (m : nat -> fol.Term L) (v : nat): In v (freeVarTs (subAllTerms n ts m)) -> exists a : nat, In a (freeVarTs ts) /\ In v (freeVarT (m a)).
proof: Proof. induction ts as [| n t ts Hrects]. - intros H; contradiction. - intros H; simpl in H. unfold freeVarTs in H; fold (freeVarT (subAllTerm t m)) in H; fold (freeVarTs (subAllTerms n ts m)) in H. induction (in_app_or _ _ _ H) as [H0 | H0]. + induction (freeVarSubAllTerm1 _ _ _ H0) as [x H1]; exists x; split. * unfold freeVarTs; fold (freeVarT t); fold (freeVarTs ts). apply in_or_app; tauto. * tauto. + induction (Hrects H0) as [x H1]; exists x; split. * unfold freeVarTs; fold (freeVarT t); fold (freeVarTs ts). apply in_or_app; tauto. * tauto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)