...

[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..8605105bf8e597c021761b0e45d3b7854ac268d3 100644 (file)
--- a/helm/software/matita/library/dama/property_exhaustivity.ma
+++ b/helm/software/matita/library/dama/property_exhaustivity.ma
@@ -28,8 +28,8 @@ qed.
 notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
 notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
 
-interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
-interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
+interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l ?)).
+interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r ?)).
 
 lemma h_segment_preserves_uparrow:
   ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
@@ -45,8 +45,8 @@ qed.
 notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
 notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
 
-interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
-interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
+interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l ?)).
+interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r ?)).
  
 (* Fact 2.18 *)
 lemma segment_cauchy:
@@ -90,9 +90,10 @@ qed.
 notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.
 notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'downarrow_to_in_segment}.
 
-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 _)).
+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: