- 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 a1bae198b707723b66f5ba16db61ac1cac58deab..ff190e5e3c2d2fb1ef7b952638e85e5f4f011f6e 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,10 +11,18 @@
 
 include "basics/logic.ma".
 
+(********** predicates *********)
+
+definition predicate: Type[0] → Type[0]
+≝ λA.A→Prop.
+
 (********** relations **********)
 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.