X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fexcedence.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fexcedence.ma;h=3b2afd5dc982b86c8a8308018b72bc599bc04fc2;hb=66faca1dc849662e27d760b950294ef66a5741b3;hp=950639fed11a8e0c0cc6e7b6f3fc53981bd8fcbd;hpb=3ab8f327eb6f492a7780b2309beb495e22f2bba0;p=helm.git

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 950639fed..3b2afd5dc 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -79,22 +79,22 @@ lemma eq_reflexive:∀E. reflexive ? (eq E).
 intros (E); unfold; intros (x); apply ap_coreflexive; 
 qed.
 
-lemma eq_symmetric:∀E.symmetric ? (eq E).
+lemma eq_sym_:∀E.symmetric ? (eq E).
 intros (E); unfold; intros (x y Exy); unfold; unfold; intros (Ayx); apply Exy;
 apply ap_symmetric; assumption; 
 qed.
 
-lemma eq_symmetric_:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_symmetric.
+lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_sym_.
 
-coercion cic:/matita/excedence/eq_symmetric_.con.
+coercion cic:/matita/excedence/eq_sym.con.
 
-lemma eq_transitive_: ∀E.transitive ? (eq E).
+lemma eq_trans_: ∀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_.
+lemma eq_trans:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_trans_.
 
 (* BUG: vedere se ricapita *)
 lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?).