V_______________________________________________________________ *)
include "basics/logic.ma".
+include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/subseteq_2.ma".
(********** predicates *********)
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 ≝