proposition: Lemma dsub'_strext : forall (X : CPsMetricSpace) (P : X -> CProp) (x : X), fun_strext (dsub' P x).
proof: Proof. intros X P x. unfold fun_strext in |- *. intros x0 y. unfold dsub' in |- *. case y. case x0. intros a b c d. simpl in |- *. intro H. set (H1 := csbf_strext _ _ _ (cms_d (c:=X)) _ _ _ _ H) in *. elim H1. intuition. intro H2. set (H3 := ap_irreflexive_unfolded X x H2) in *. intuition. Qed.
imports: CoRN.metrics.IR_CPMSpace