ordered_sets are built with excedence

diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma
index 5ae4f564acf208ead754c0b1da40ab8fc329f6f9..3424edbb57ee42a840a565488c821d667892ae5f 100644 (file)
--- 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;