Porting alla nuova def. di negazione

diff --git a/helm/software/matita/nlibrary/basics/functions.ma b/helm/software/matita/nlibrary/basics/functions.ma
index a4a8f240d5e89d8c10866956f9c8010e5a6d8146..186aee41da4c943cc2d092ebdc4a58d530f9c2e6 100644 (file)
--- a/helm/software/matita/nlibrary/basics/functions.ma
+++ b/helm/software/matita/nlibrary/basics/functions.ma
@@ -36,11 +36,12 @@ ndefinition symmetric2: ∀A,B:Type[0].∀f:A→A→B.Prop
 ndefinition associative: ∀A:Type[0].∀f:A→A→A.Prop
 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
 
+(*
 ntheorem eq_f_g_h:
   ∀A,B,C,D:Type[0].∀f:C→D.∀g:B→C.∀h:A→B.
   f∘(g∘h) = (f∘g)∘h.
   //.
-nqed.
+nqed. *)
 
 (* functions and relations *)
 ndefinition monotonic : ∀A:Type.∀R:A→A→Prop.

diff --git a/helm/software/matita/nlibrary/basics/relations.ma b/helm/software/matita/nlibrary/basics/relations.ma
index e70a5877aa5cafa1f58c6b09040d94eba4549910..9a01823bec70fb4652c64465281e090dfb20014c 100644 (file)
--- a/helm/software/matita/nlibrary/basics/relations.ma
+++ b/helm/software/matita/nlibrary/basics/relations.ma
@@ -17,6 +17,9 @@ include "Plogic/connectives.ma".
 ndefinition relation : Type \to Type
 ≝ λA:Type.A→A→Prop. 
 
+nrecord relation (A:Type) : Type ≝
+{fun:2> A→A→Prop}.
+
 ndefinition reflexive: ∀A:Type.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.