X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=d40856195681e6b2e357488658619f06265ee965;hb=143c97a8fe657eb7b041dec2747b0e67b5899762;hp=84dd7c362bf7a86e590fc474130372bbc5e703f7;hpb=e5077c96c584933ad1467e8066780b46d7b0468c;p=helm.git

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 84dd7c362..d40856195 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -191,3 +191,9 @@ definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
 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.
+
+definition bi_RC: ∀A,B:Type[0]. bi_relation A B → bi_relation A B ≝
+                  λA,B,R,x1,y1,x2,y2. R … x1 y1 x2 y2 ∨ (x1 = x2 ∧ y1 = y2).
+
+lemma bi_RC_reflexive: ∀A,B,R. bi_reflexive A B (bi_RC … R).
+/3 width=1/ qed.