proposition: Lemma map_eq : forall (g : A->B) l, (forall x, In x l -> f x = g x) -> map f l = map g l.
proof: Proof. induction l; simpl; intros. refl. apply cons_eq. ded (H a). intuition. apply IHl. intro. ded (H x). intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)