X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fmodels%2Fnat_lebesgue.ma;h=2657aba89dd37f3f76645fdd7fcc81f0aafbe0bf;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=8d563b1e351d469c4cb2097dda9fcd094b689915;hpb=c5a4db6c1020488d0792cee00dcf395a0ce54735;p=helm.git

diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma
index 8d563b1e3..2657aba89 100644
--- a/helm/software/matita/library/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma
@@ -15,6 +15,7 @@
 include "dama/lebesgue.ma".
 include "dama/models/nat_order_continuous.ma".
 
+alias symbol "dependent_pair" = "dependent pair".
 theorem nat_lebesgue_oc:
    ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. 
      ∀x:ℕ.a order_converges x →