X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fconstructive_higher_order_relations.ma;h=cf58e2640ec6a6472dd9731286cd9d0bfcdb9b9b;hb=12ebc9483bec78f948de80e7e230c98488890f4d;hp=b66ba684309c47c2cb606f2607e4db506b374f31;hpb=2ab6644dd2dff227ac1bf335df7ff0d244ebe8dc;p=helm.git

diff --git a/helm/software/matita/dama/constructive_higher_order_relations.ma b/helm/software/matita/dama/constructive_higher_order_relations.ma
index b66ba6843..cf58e2640 100644
--- a/helm/software/matita/dama/constructive_higher_order_relations.ma
+++ b/helm/software/matita/dama/constructive_higher_order_relations.ma
@@ -29,3 +29,9 @@ definition symmetric ≝
 
 definition transitive ≝
  λC:Type.λle:C→C→Type.∀x,y,z:C.le x y → le y z → le x z.
+
+definition associative ≝
+ λC:Type.λop:C→C→C.λeq:C→C→Type.∀x,y,z. eq (op x (op y z)) (op (op x y) z).
+
+definition commutative ≝
+ λC:Type.λop:C→C→C.λeq:C→C→Type.∀x,y. eq (op x y) (op y x).