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