proposition: Lemma map_eq : forall (A B : Type) (f g : A -> B) l, (forall a, In a l -> f a = g a) -> map f l = map g l.
proof: Proof. intros A B f g l; induction l as [ | a l]; intros H; trivial. simpl; rewrite (H a). rewrite IHl; trivial. intros; apply H; right; trivial. left; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)