proposition: Lemma is_P : forall (P : IR -> CProp) (l : list (SubPsMetricSpace IR_as_CPsMetricSpace P)) (x : IR), pred_wd IR P -> member x (list_IR P l) -> P x.
proof: Proof. intros P l x Q. induction l as [| a l Hrecl]. simpl in |- *. intuition. case a. simpl in |- *. intros b C D. elim D. intro E. apply Hrecl. exact E. unfold pred_wd in Q. intro H. apply Q with b. exact C. apply eq_symmetric_unfolded. exact H. Qed.
imports: CoRN.metrics.Prod_Sub