X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fbishop_set_rewrite.ma;h=ff063e29a0adaaeed17bb1f6d9ad0404970a082b;hb=179574c117d34a39cebeaa66673cda83974e135a;hp=7ead93370f36a5609c6839b4d80c25ef979d4f91;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
index 7ead93370..ff063e29a 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
@@ -14,7 +14,7 @@
 
 include "bishop_set.ma".
 
-coercion cic:/matita/dama/bishop_set/eq_sym.con.
+coercion eq_sym.
 
 lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ 
   λE,x,y,z.eq_trans_ E x z y.
@@ -25,12 +25,12 @@ notation > "'Eq'≈" non associative with precedence 50
 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);
+intros (E z y x Exy Lxz); apply (le_transitive ??? ? Lxz);
 intro Xyz; apply Exy; right; assumption;
 qed.
 
 lemma le_rewr: ∀E:ordered_set.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
-intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
+intros (E z y x Exy Lxz); apply (le_transitive ??? Lxz);
 intro Xyz; apply Exy; left; assumption;
 qed.
 
@@ -55,12 +55,12 @@ notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
 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 (os_cotransitive ??? x Ayz); [2:assumption]
+intros (A x z y Exy Ayz); cases (exc_cotransitive ?? x Ayz); [2:assumption]
 cases Exy; right; assumption;
 qed.
   
 lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
-intros (A x z y Exy Azy); cases (os_cotransitive ???x Azy); [assumption]
+intros (A x z y Exy Azy); cases (exc_cotransitive ??x Azy); [assumption]
 cases (Exy); left; assumption;
 qed.
 
@@ -69,7 +69,7 @@ interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl _ _ _).
 notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
 interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr _ _ _).
 
-
+(*
 lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
 intros (A x y z E H); split; cases H;
 [apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
@@ -84,4 +84,4 @@ notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
 interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
 interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
-
+*)