proposition: Lemma subAllFormula_ext : forall (f : fol.Formula L) (m1 m2 : nat -> fol.Term L), (forall m : nat, In m (freeVarF f) -> m1 m = m2 m) -> subAllFormula f m1 = subAllFormula f m2.
proof: Proof. intro f; induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl. - intros m1 m2 H; rewrite (subAllTerm_ext t m1 m2). + rewrite (subAllTerm_ext t0 m1 m2). * reflexivity. * intros m H0; apply H. apply in_or_app; auto. + intros m H0; apply H. apply in_or_app; auto. - intros m1 m2 H; rewrite (subAllTerms_ext _ t m1 m2). + reflexivity. + apply H. - intros m1 m2 H; rewrite (Hrecf1 m1 m2). + rewrite (Hrecf0 m1 m2). * reflexivity. * intros m H0; apply H. apply in_or_app; auto. + intros m H0; apply H. apply in_or_app; auto. - intros m1 m2 H; rewrite (Hrecf m1 m2). + reflexivity. + apply H. - intros m1 m2 H; rewrite (freeVarMap_ext (List.remove eq_nat_dec n (freeVarF f)) m1 m2). + set (m1' := fun v : nat => match eq_nat_dec v n with | left _ => var (newVar (freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) m2)) | right _ => m1 v end). set (m2' := fun v : nat => match eq_nat_dec v n with | left _ => var (newVar (freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) m2)) | right _ => m2 v end). rewrite (Hrecf m1' m2'). * reflexivity. * intros m H0; unfold m1', m2'; clear m1' m2'. induction (eq_nat_dec m n). -- reflexivity. -- apply H; apply in_in_remove; auto. + intros m H0; apply H, H0. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)