...

[helm.git] / helm / software / matita / contribs / dama / dama / bishop_set_rewrite.ma

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 7ead93370f36a5609c6839b4d80c25ef979d4f91..27bb10f5a858a971721740b297c77bd5f879998e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
@@ -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 (hos_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 (hos_cotransitive ???x Azy); [assumption]
 cases (Exy); left; assumption;
 qed.