X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fproperty_exhaustivity.ma;h=0d35ca981b8d864692376b0d6dd0e4bc6ab6a81b;hb=6090d3df71fdd405d231981c8bf2aedff01612c5;hp=4dec6442e0fd8e26ae995e3de4ef045968a014c1;hpb=c5a4db6c1020488d0792cee00dcf395a0ce54735;p=helm.git

diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma
index 4dec6442e..0d35ca981 100644
--- a/helm/software/matita/library/dama/property_exhaustivity.ma
+++ b/helm/software/matita/library/dama/property_exhaustivity.ma
@@ -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.