proposition: Lemma freeVarSubAllFormula2 : forall (f : fol.Formula L) (m : nat -> fol.Term L) (v n : nat), In n (freeVarF f) -> In v (freeVarT (m n)) -> In v (freeVarF (subAllFormula f m)).
proof: Proof. intro f; induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl. - intros m v n H H0; apply in_or_app. induction (in_app_or _ _ _ H) as [H1 | H1]. + left; eapply freeVarSubAllTerm2. * apply H1. * apply H0. + right; eapply freeVarSubAllTerm2. * apply H1. * apply H0. - intros m v n H H0; eapply freeVarSubAllTerms2. + apply H. + apply H0. - intros m v n H H0; apply in_or_app. induction (in_app_or _ _ _ H) as [H1 | H1]. + left; eapply Hrecf1. * apply H1. * apply H0. + right; eapply Hrecf0. * apply H1. * apply H0. - intros m v n H H0; eapply Hrecf. + apply H. + apply H0. - intros m v n0 H H0; apply in_in_remove. + intro H1; eapply (newVar1 (freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) m)). rewrite <- H1; clear H1; apply in_or_app. right. clear Hrecf. induction (List.remove eq_nat_dec n (freeVarF f)); simpl in |- *. * contradiction H. * apply in_or_app; simpl in H. destruct H as [H | H]. -- rewrite H; auto. -- auto. + eapply Hrecf. * eapply in_remove; apply H. * induction (eq_nat_dec n0 n) as [a | b]. -- now elim (in_remove_neq _ _ _ _ _ H). -- auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)