Simplified proof after pattern fix

[helm.git] / helm / software / matita / nlibrary / basics / relations.ma

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.