snapshot

[helm.git] / matita / dama / constructive_higher_order_relations.ma

diff --git a/matita/dama/constructive_higher_order_relations.ma b/matita/dama/constructive_higher_order_relations.ma
index b66ba684309c47c2cb606f2607e4db506b374f31..cf58e2640ec6a6472dd9731286cd9d0bfcdb9b9b 100644 (file)
--- 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).