proposition: Lemma freeVarSubTerm2 (t : Term) : forall (v : nat) (s : Term) (x : nat), In x (freeVarT s) -> In v (freeVarT t) -> In x (freeVarT (substT t v s)).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => forall (v : nat) (s : Term) (x : nat), In x (freeVarT s) -> In v (freeVarTs ts) -> In x (freeVarTs (substTs ts v s))). - intros n v s x H H0; simpl; induction (eq_nat_dec v n) as [? | b]. + assumption. + elim b; induction H0 as [H0| H0]. * auto. * contradiction. - intros f t0 H v s x H0 H1; simpl; unfold freeVarT; fold (freeVarTs (substTs t0 v s)). apply H; auto. - intros v s x H H0; auto. - intros n t0 H t1 H0 v s x H1 H2; simpl; unfold freeVarTs in H2; fold (freeVarT t0) in H2; fold (freeVarTs t1) in H2. unfold freeVarTs; fold (freeVarT (substT t0 v s)); fold (freeVarTs (substTs t1 v s)); apply in_or_app. induction (in_app_or _ _ _ H2). + left; apply H; auto. + right; apply H0; auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)