proposition: Lemma emb_strext : forall X : CPsMetricSpace, fun_strext (emb X).
proof: Proof. intro X. unfold fun_strext in |- *. unfold emb in |- *. simpl in |- *. unfold metric_ap in |- *. apply ax_d_pos_imp_ap. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv