added mactions, the three can now be collapsed to fit the screen

[helm.git] / helm / software / matita / library / dama / property_exhaustivity.ma

diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma
index deddf88049f5e60a2108942506b67a65bf79bf80..0d35ca981b8d864692376b0d6dd0e4bc6ab6a81b 100644 (file)
--- a/helm/software/matita/library/dama/property_exhaustivity.ma
+++ b/helm/software/matita/library/dama/property_exhaustivity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_uniform.ma".
-include "property_sigma.ma".
+include "dama/ordered_uniform.ma".
+include "dama/property_sigma.ma".
 
 lemma h_segment_upperbound:
   ∀C:half_ordered_set.
@@ -93,6 +93,7 @@ notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'d
 interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)).
 interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)).
  
+alias symbol "dependent_pair" = "dependent pair".
 (* Lemma 3.8 NON DUALIZZATO *)
 lemma restrict_uniform_convergence_uparrow:
   ∀C:ordered_uniform_space.property_sigma C →
@@ -105,17 +106,17 @@ intros; split;
     simplify; intros; cases (a i); assumption;
 |2: intros;
     lapply (uparrow_upperlocated a ≪x,h≫) as Ha1;
-      [2: apply (segment_preserves_uparrow s); assumption;] 
+      [2: apply (segment_preserves_uparrow s); assumption;]
     lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2; 
     cases Ha2; clear Ha2;
     cases (H1 a a); lapply (H5 H3 Ha1) as HaC;
     lapply (segment_cauchy C s ? HaC) as Ha;
     lapply (sigma_cauchy ? H  ? x ? Ha); [left; assumption]
-    apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)]
+    apply (restric_uniform_convergence C s ≪?,h≫ a Hletin)]
 qed.
 
 lemma hint_mah1:
-  ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
+  ∀C. Type_OF_ordered_uniform_space__1 C → hos_carr (os_r C).
   intros; assumption; qed.
   
 coercion hint_mah1 nocomposites.