notation > "'Eq'≈" non associative with precedence 50
for @{'eqrewrite}.
-interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
+interpretation "eq_rew" 'eqrewrite = (eq_trans ? ? ?).
lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
intros (E z y x Exy Lxz); apply (le_transitive ??? ? Lxz);
qed.
notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
+interpretation "le_rewl" 'lerewritel = (le_rewl ? ? ?).
notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
+interpretation "le_rewr" 'lerewriter = (le_rewr ? ? ?).
lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
qed.
notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
+interpretation "ap_rewl" 'aprewritel = (ap_rewl ? ? ?).
notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
+interpretation "ap_rewr" 'aprewriter = (ap_rewr ? ? ?).
lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
intros (A x z y Exy Ayz); cases (exc_cotransitive ?? x Ayz); [2:assumption]
qed.
notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
-interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl _ _ _).
+interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl ? ? ?).
notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
-interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr _ _ _).
+interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr ? ? ?).
(*
lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
qed.
notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl ? ? ?).
notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr ? ? ?).
*)