proposition: Lemma freeVarSubAllTerm2 (t : fol.Term L) (m : nat -> fol.Term L) (v n : nat): In n (freeVarT t) -> In v (freeVarT (m n)) -> In v (freeVarT (subAllTerm t m)).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (a : nat) (ts : fol.Terms L a) => In n (freeVarTs ts) -> In v (freeVarT (m n)) -> In v (freeVarTs (subAllTerms a ts m))). - intros n0 [H | H] H0; simpl in H |- *. + now rewrite H. + contradiction H. - auto. - auto. - intros n0 t0 H t1 H0 H1 H2; simpl; unfold freeVarTs; fold (freeVarT (subAllTerm t0 m)). fold (freeVarTs (subAllTerms n0 t1 m)); apply in_or_app. unfold freeVarTs in H1. fold (freeVarT t0) in H1. fold (freeVarTs t1) in H1. induction (in_app_or _ _ _ H1); auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)