-definition apart_metric:=
- λR.λms:metric_space R.λa,b:ms.0 < δ a b.
-
-lemma apart_of_metric_space: ∀R:ogroup.metric_space R → apartness.
-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);
+lemma apart_of_metric_space: ∀R.metric_space R → apartness.
+intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
+[1: intros 2 (x H); cases H (H1 H2); clear H;
+ lapply (Ap≫ ? (eq_sym ??? (mreflexive ??x)) H2);