ocaml 3.09 transition

[helm.git] / helm / matita / library / higher_order_defs / relations.ma

diff --git a/helm/matita/library/higher_order_defs/relations.ma b/helm/matita/library/higher_order_defs/relations.ma
index ff75c9d9569cbd277eaaa500f4eac4eb0f833e73..029b229dc0f518edc78bca16ad317bd326ce59bb 100644 (file)
--- a/helm/matita/library/higher_order_defs/relations.ma
+++ b/helm/matita/library/higher_order_defs/relations.ma
@@ -28,3 +28,6 @@ definition transitive: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
 \lambda A.\lambda R.\forall x,y,z:A.R x y \to R y z \to R x z.
 
+definition irreflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop
+\def 
+\lambda A.\lambda R.\forall x:A.\lnot (R x x).