+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 ≝
+ λ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.
+interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
+
+definition Runion ≝ λA.λR1,R2:relation A.λa,b. R1 a b ∨ R2 a b.
+interpretation "union of relations" 'union R1 R2 = (Runion ? R1 R2).
+
+definition Rintersection ≝ λA.λR1,R2:relation A.λa,b.R1 a b ∧ R2 a b.
+interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? R1 R2).
+
+definition inv ≝ λA.λR:relation A.λa,b.R b a.
+
+(*********** sub relation ***********)
+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/
+qed.
+
+lemma sub_comp_r: ∀A.∀R,R1,R2:relation A.
+ R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2.
+#A #R #R1 #R2 #Hsub #a #b * #c * /4/
+qed.
+
+lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A.
+ R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3.
+#A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/
+qed.
+
+lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A.
+ (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3).
+#A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/
+qed.
+
+(************* functions ************)