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