X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=ff190e5e3c2d2fb1ef7b952638e85e5f4f011f6e;hb=1185204d6a1e634a107fac71a45c9f87f49ccc31;hp=a82f314f698e9dc23fb479c56848c83b586d2654;hpb=aacce10080ef24f9851d760294c3e5d8233440cc;p=helm.git

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index a82f314f6..ff190e5e3 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,7 +11,7 @@
 
 include "basics/logic.ma".
 
-(********** preducates *********)
+(********** predicates *********)
 
 definition predicate: Type[0] → Type[0]
 ≝ λA.A→Prop.
@@ -20,6 +20,9 @@ definition predicate: Type[0] → Type[0]
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
 
+definition relation2 : Type[0] → Type[0] → Type[0]
+≝ λA,B.A→B→Prop.
+
 definition reflexive: ∀A.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.