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

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index b31db23d7..a82f314f6 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,6 +11,11 @@
 
 include "basics/logic.ma".
 
+(********** preducates *********)
+
+definition predicate: Type[0] → Type[0]
+≝ λA.A→Prop.
+
 (********** relations **********)
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
@@ -73,12 +78,13 @@ definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
 
 lemma injective_compose : ∀A,B,C,f,g.
 injective A B f → injective B C g → injective A C (λx.g (f x)).
-/3/; qed.
+/3/; qed-.
 
 (* extensional equality *)
 
+(* moved inside sets.ma
 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
-λA.λP,Q.∀a.iff (P a) (Q a).
+λA.λP,Q.∀a.iff (P a) (Q a). *)
 
 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
@@ -86,11 +92,12 @@ definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
 λA,B.λf,g.∀a.f a = g a.
 
+(*
 notation " x \eqP y " non associative with precedence 45 
 for @{'eqP A $x $y}.
 
 interpretation "functional extentional equality" 
-'eqP A x y = (exteqP A x y).
+'eqP A x y = (exteqP A x y). *)
 
 notation "x \eqR y" non associative with precedence 45 
 for @{'eqR ? ? x y}.