update in groud_2 and models

[helm.git] / helm / software / matita / library / dama / models / nat_lebesgue.ma

diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma
index d5e65215ec43a4bdaa3bc18be7d10acad54555c5..2657aba89dd37f3f76645fdd7fcc81f0aafbe0bf 100644 (file)
--- a/helm/software/matita/library/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lebesgue.ma".
-include "models/nat_order_continuous.ma".
+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 →