definition relation2 : Type[0] → Type[0] → Type[0]
≝ λA,B.A→B→Prop.
+definition relation3 : Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C.A→B→C→Prop.
+
definition reflexive: ∀A.∀R :relation A.Prop
≝ λA.λR.∀x:A.R x x.
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.
+
+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 confluent: ∀A. predicate (relation A) ≝ λA,R.
+ ∀a0. confluent1 … R a0.
+
+(* Reflexive closure ************)
+
+definition RC: ∀A:Type[0]. relation A → relation A ≝
+ λA,R,x,y. R … x y ∨ x = y.
+
+lemma RC_reflexive: ∀A,R. reflexive A (RC … R).
+/2 width=1/ qed.
+
(********** operations **********)
definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
∃am.R1 a1 am ∧ R2 am a2.
definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
+lemma sub_reflexive :
+ ∀T.∀R:relation T.R ⊆ R.
+#T #R #x //
+qed.
+
lemma sub_comp_l: ∀A.∀R,R1,R2:relation A.
R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
#A #R #R1 #R2 #Hsub #a #b * #c * /4/
interpretation "functional extentional equality"
'eqF A B f g = (exteqF A B f g).
+(********** relations on unboxed pairs **********)
+
+definition bi_relation: Type[0] → Type[0] → Type[0]
+≝ λA,B.A→B→A→B→Prop.
+
+definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
+≝ λA,B,R. ∀x,y. R x y x y.
+
+definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+ ∀a1,a2,b1,b2. R a2 b2 a1 b1 → R a1 b1 a2 b2.
+
+definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+ ∀a1,a,b1,b. R a1 b1 a b →
+ ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.