X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fexcedence.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fexcedence.ma;h=735fe2262828da3ce9bc1cf8dd892cd062ea9369;hb=0b57df2b9578e65c733df29ed6fa00c047a606e8;hp=84a033c3a8ebb071bf2b56abca7b4fa1bbf8a873;hpb=21b202653d14ba7d8139f44c495fde94f8cb345c;p=helm.git

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 84a033c3a..735fe2262 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -88,12 +88,14 @@ lemma eq_symmetric_:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_symmetric.
 
 coercion cic:/matita/excedence/eq_symmetric_.con.
 
-lemma eq_transitive: ∀E.transitive ? (eq E).
+lemma eq_transitive_: ∀E.transitive ? (eq E).
 (* bug. intros k deve fare whd quanto basta *)
 intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy); 
 [apply Exy|apply Eyz] assumption.
 qed.
 
+lemma eq_transitive:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_transitive_.
+
 (* BUG: vedere se ricapita *)
 lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?).
 intros 5 (E x y Lxy Lyx); intro H;