proposition: Lemma member1 : forall (P : IR -> CProp) (x0 : subcsetoid_crr IR P) (l : list (SubPsMetricSpace IR_as_CPsMetricSpace P)), MSmember (X:=SubPsMetricSpace IR_as_CPsMetricSpace P) x0 l -> member (to_IR P x0) (list_IR P l).
proof: Proof. intros P x0 l. induction l as [| a l Hrecl]. simpl in |- *. intuition. simpl in |- *. intros H. elim H. intro H1. left. apply Hrecl. exact H1. simpl in |- *. intros. right. rewrite b. intuition. Qed.
imports: CoRN.metrics.Prod_Sub