proposition: Lemma freeVarSubTerms2 (n : nat) (ts : Terms n) (v : nat) (s : Term) (x : nat): In x (freeVarT s) -> In v (freeVarTs ts) -> In x (freeVarTs (substTs ts v s)).
proof: Proof. intros H H0; induction ts as [| n t ts Hrects]. - contradiction H0. - simpl; unfold freeVarTs in H0; fold (freeVarT t) in H0. fold (freeVarTs ts) in H0; unfold freeVarTs. fold (freeVarT (substT t v s)); fold (freeVarTs (substTs ts v s)); apply in_or_app. destruct (in_app_or _ _ _ H0). + left; apply freeVarSubTerm2; auto. + right; apply Hrects; auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)