X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=9da779ee45db629c6994b682d7852c011e553701;hb=7c9d99dfb049d726491b71f07ba6a9b088b30166;hp=24b2c9a9e32b688c05c712cd824a390ba2f65a76;hpb=b5cb5cc7230870f757aadbe6b43ee146fe485a6d;p=helm.git

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 24b2c9a9e..9da779ee4 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,6 +11,7 @@
 
 include "basics/logic.ma".
 include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/subseteq_2.ma".
 
 (********** predicates *********)
 
@@ -55,12 +56,12 @@ definition antisymmetric: ∀A.∀R:relation A.Prop
 definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
                          ∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
 
-definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
-                       ∀a1. R a0 a1 → ∀a2. R a0 a2 →
-                       ∃∃a. R a1 a & R a2 a. 
+definition pw_confluent: ∀A. relation A → predicate A ≝ λA,R,a0.
+                         ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+                         ∃∃a. R a1 a & R a2 a. 
 
 definition confluent: ∀A. predicate (relation A) ≝ λA,R.
-                      ∀a0. confluent1 … R a0.
+                      ∀a0. pw_confluent … R a0.
 
 (* triangular confluence of two relations *)
 definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.