decentralizing core notation

[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 a43ed63252a37e64c768326422f7dae3147678c4..24b2c9a9e32b688c05c712cd824a390ba2f65a76 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "basics/logic.ma".
+include "basics/core_notation/compose_2.ma".
 
 (********** predicates *********)
 
@@ -61,6 +62,10 @@ definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
 definition confluent: ∀A. predicate (relation A) ≝ λA,R.
                       ∀a0. confluent1 … R a0.
 
+(* triangular confluence of two relations *)
+definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
+                  ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b.
+
 (* Reflexive closure ************)
 
 definition RC: ∀A:Type[0]. relation A → relation A ≝