X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fconstructive_higher_order_relations.ma;fp=matita%2Fdama%2Fconstructive_higher_order_relations.ma;h=cf58e2640ec6a6472dd9731286cd9d0bfcdb9b9b;hb=b0b85f3cad753caba19e785e09cc10ff8a6c00d9;hp=b66ba684309c47c2cb606f2607e4db506b374f31;hpb=5c0c5980586c1fc530fd304275607dd2f8afeba0;p=helm.git

diff --git a/matita/dama/constructive_higher_order_relations.ma b/matita/dama/constructive_higher_order_relations.ma
index b66ba6843..cf58e2640 100644
--- a/matita/dama/constructive_higher_order_relations.ma
+++ b/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).