X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Frelations.ma;h=9a01823bec70fb4652c64465281e090dfb20014c;hb=b1736386d7728463cfcc7b3539633db9154809b5;hp=e70a5877aa5cafa1f58c6b09040d94eba4549910;hpb=3bd88fb8b932e2f76762e8068b19745167cb1ce1;p=helm.git

diff --git a/helm/software/matita/nlibrary/basics/relations.ma b/helm/software/matita/nlibrary/basics/relations.ma
index e70a5877a..9a01823be 100644
--- 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.