minor changes to make the library compile after wilmers new exists.

[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 f76660190d59476dca1d8bef9c1e0fb8bdc3e879..0d35ca981b8d864692376b0d6dd0e4bc6ab6a81b 100644 (file)
--- 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,13 +106,13 @@ 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: