From 6f2fb1a1d58a4cf5c8ebccf916bd94da013087f7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 12 Nov 2007 16:41:30 +0000 Subject: [PATCH] ordered_sets are built with excedence --- helm/software/matita/dama/ordered_sets.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma index 5ae4f564a..3424edbb5 100644 --- a/helm/software/matita/dama/ordered_sets.ma +++ b/helm/software/matita/dama/ordered_sets.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/ordered_sets/". -include "ordered_sets.ma". +include "excedence.ma". record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ { por_reflexive: reflexive ? le; -- 2.39.2