proposition: Lemma freeVarMap_ext (l : list nat) (f1 f2 : nat -> fol.Term L): (forall m : nat, In m l -> f1 m = f2 m) -> freeVarMap l f1 = freeVarMap l f2.
proof: Proof. intros H; induction l as [| a l Hrecl]. - reflexivity. - simpl; rewrite Hrecl, H. + reflexivity. + auto with datatypes. + intros m H0; apply H; auto with datatypes. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)