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).
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:
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 *)