proposition: Lemma subAllTerms_ext (n : nat) (ts : fol.Terms L n) (m1 m2 : nat -> fol.Term L): (forall m : nat, In m (freeVarTs ts) -> m1 m = m2 m) -> subAllTerms n ts m1 = subAllTerms n ts m2.
proof: Proof. intros H; induction ts as [| n t ts Hrects]. - reflexivity. - simpl; rewrite Hrects. + rewrite (subAllTerm_ext t m1 m2); [reflexivity| ]. intros m H0; apply H. unfold freeVarTs; fold (freeVarTs ts); apply in_or_app; auto. + intros m H0; apply H. unfold freeVarTs; fold (freeVarTs ts); apply in_or_app; auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)