proposition: Lemma map_ext_in : 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 [|? ? IHl]; simpl; auto. intros H; rewrite H by intuition; rewrite IHl; auto. Qed.
imports: PeanoNat