X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=ed5130955886e557a1e11b8c83b09f7ad649cb48;hb=eae50cc815292d335df1c488a00b39ef98fa5870;hp=f469ddca29f72fe1eeaeea9d50752fefed34aad2;hpb=a04bfe6d381b281db15e8b432f6f221576aad439;p=helm.git

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index f469ddca2..ed5130955 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -48,6 +48,14 @@ definition tight_apart: ∀A.∀eq,ap:relation A.Prop
 definition antisymmetric: ∀A.∀R:relation A.Prop
 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
 
+(* 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.