- basics: bug fix in Conf3, it was not generic enough

[helm.git] / matita / matita / lib / basics / relations.ma

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index a82f314f698e9dc23fb479c56848c83b586d2654..ff190e5e3c2d2fb1ef7b952638e85e5f4f011f6e 100644 (file)
--- 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.