intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
[1: intros 2 (x H); cases H (H1 H2);
lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);
intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
[1: intros 2 (x H); cases H (H1 H2);
lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);