X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;h=2ea43c03ae11017df5c262218a41b570ff11c15a;hb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;hp=bd16b2bd60217b33208159b97e188c99c2b06ee3;hpb=b3dd479a0a36aeea948dcea09336fe8dfec1462d;p=helm.git

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index bd16b2bd6..2ea43c03a 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -49,5 +49,5 @@ qed.
     
 (* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
 
-lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.x#y → 0 < δ x y.
+lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
 intros 2 (R m); cases m 0; simplify; intros; assumption; qed.