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

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index afb5d5aae..f469ddca2 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -23,6 +23,9 @@ definition relation : Type[0] → Type[0]
 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.
 
@@ -161,5 +164,12 @@ interpretation "functional extentional equality"
 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
+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.