proposition: Lemma freeVarSubTerm1 (t : Term): forall (v : nat) (s : Term) (x : nat), In x (freeVarT t) -> v <> x -> 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 (freeVarTs ts) -> v <> x -> In x (freeVarTs (substTs ts v s))). - intros n v s x H H0; simpl. induction (eq_nat_dec v n) as [? | ?]. + destruct H0; simpl in H; induction H as [H| H]. * congruence. * contradiction. + assumption. - intros f t0 H v s x H0 H1; simpl in |- *. unfold freeVarT; apply H; auto. - intros; auto. - intros n t0 H t1 H0 v s x H1 H2; unfold freeVarTs in H1. induction (in_app_or _ _ _ H1); unfold freeVarTs; simpl; apply in_or_app; auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)