proposition: Lemma freeVarSubAllFormula1 : forall (f : fol.Formula L) (m : nat -> fol.Term L) (v : nat), In v (freeVarF (subAllFormula f m)) -> exists n : nat, In n (freeVarF f) /\ In v (freeVarT (m n)).
proof: Proof. intro f; induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl. - intros m v H; induction (in_app_or _ _ _ H); (induction (freeVarSubAllTerm1 _ _ _ H0); exists x; split; [ apply in_or_app; tauto | tauto ]). - intros m v H; apply freeVarSubAllTerms1; apply H. - intros m v H; induction (in_app_or _ _ _ H) as [H0 | H0]; (induction (Hrecf1 _ _ H0) || induction (Hrecf0 _ _ H0); exists x; split; [ apply in_or_app; tauto | tauto ]). - intros m v H; apply Hrecf. apply H. - intros m v H; set (nv := newVar (freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) m)). assert (H0: In v (freeVarF (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var nv | right _ => m v end)))) by ( eapply in_remove; apply H). destruct (Hrecf _ _ H0) as [x [H2 H3]]. induction (eq_nat_dec x n) as [a | ?]. + elim (in_remove_neq _ _ _ _ _ H). induction H3 as [H1| H1]. auto. contradiction. + exists x. split. * apply in_in_remove; auto. * auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)