proposition: Lemma freeVarSubTerm4 (t : Term) : forall (v : nat) (s : Term) (x : nat), In x (freeVarT (substT t v s)) -> ~ In v (freeVarT t) -> In x (freeVarT t).
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 (substTs ts v s)) -> ~ In v (freeVarTs ts) -> In x (freeVarTs ts)). - intros n v s x H H0; simpl in H |- *. induction (eq_nat_dec v n) as [a | ?]. + elim H0; rewrite a; simpl; now left. + apply H. - intros f t0 H v s x H0 H1; simpl in H0; eapply H. + apply H0. + apply H1. - intros; assumption. - intros n t0 H t1 H0 v s x H1 H2; simpl in H1. unfold freeVarTs in H1; fold (freeVarT (substT t0 v s)) in H1; fold (freeVarTs (substTs t1 v s)) in H1; unfold freeVarTs ; fold (freeVarT t0); fold (freeVarTs t1). induction (in_app_or _ _ _ H1) as [H3 | H3]. + apply in_or_app; left; eapply H. * apply H3. * intro H4; elim H2. unfold freeVarTs; fold (freeVarT t0); fold (freeVarTs t1); apply in_or_app. now left. + apply in_or_app; right; eapply H0. * apply H3. * intro H4; elim H2. unfold freeVarTs; fold (freeVarT t0); fold (freeVarTs t1); apply in_or_app; now right. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)