proposition: Lemma map_member : forall (X Z : CPsMetricSpace) (f : X -> Z) (l : list X) (m : X), MSmember m l -> MSmember (f m) (map f l).
proof: Proof. intros X Z f l m. induction l as [| a l Hrecl]. simpl in |- *. auto. simpl in |- *. intro H. elim H. intro H1. left. apply Hrecl. exact H1. intro H1. right. rewrite H1. intuition. Qed.
imports: CoRN.metrics.Prod_Sub