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