more cleanup

[helm.git] / matita / dama / excedence.ma

diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma
index 84a033c3a8ebb071bf2b56abca7b4fa1bbf8a873..735fe2262828da3ce9bc1cf8dd892cd062ea9369 100644 (file)
--- a/matita/dama/excedence.ma
+++ b/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;