- lambda: parallel reduction to obtain diamond property

[helm.git] / matita / matita / lib / basics / relations.ma

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index ed5130955886e557a1e11b8c83b09f7ad649cb48..8b746ef6896d4f58bb4efa17728a27b7f8bba0e7 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -48,6 +48,9 @@ definition tight_apart: ∀A.∀eq,ap:relation A.Prop
 definition antisymmetric: ∀A.∀R:relation A.Prop
 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
 
+definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
+                         ∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
+
 (* Reflexive closure ************)
 
 definition RC: ∀A:Type[0]. relation A → relation A ≝