proposition: Lemma map_member' : forall (X Z : CPsMetricSpace) (f : CSetoid_fun X Z) (l : list X) (m : X), MSmember m l -> MSmember (X:=Build_SubCSetoid Z (fun y : Z => {x0 : X | f x0[=]y})) (re_co_do X Z f m) (map (re_co_do X Z 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