X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fhigher_order_defs%2Fordering.ma;h=c2b351d7abe878a4f5064c96410ead6171dc8ffc;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a945805da1496d6156602efae9ba3e31e584073d;hpb=244d65f63ca6a736b871f9f91328fe8c5524ff05;p=helm.git

diff --git a/helm/matita/library/higher_order_defs/ordering.ma b/helm/matita/library/higher_order_defs/ordering.ma
index a945805da..c2b351d7a 100644
--- a/helm/matita/library/higher_order_defs/ordering.ma
+++ b/helm/matita/library/higher_order_defs/ordering.ma
@@ -18,5 +18,5 @@ include "logic/equality.ma".
 
 definition antisymmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
-\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to (eq A x y).
+\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to x=y.