X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fproperty_exhaustivity.ma;h=8605105bf8e597c021761b0e45d3b7854ac268d3;hb=5bed3ef9523751da77b0c57a85fd880083cde248;hp=0d35ca981b8d864692376b0d6dd0e4bc6ab6a81b;hpb=fdab21f9db0c8536718001e38213c34595170182;p=helm.git

diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma
index 0d35ca981..8605105bf 100644
--- 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,8 +90,8 @@ 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 *)