]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/dama/property_exhaustivity.ma
more ex and more notation
[helm.git] / helm / software / matita / library / dama / property_exhaustivity.ma
index deddf88049f5e60a2108942506b67a65bf79bf80..4dec6442e0fd8e26ae995e3de4ef045968a014c1 100644 (file)
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_uniform.ma".
-include "property_sigma.ma".
+include "dama/ordered_uniform.ma".
+include "dama/property_sigma.ma".
 
 lemma h_segment_upperbound:
   ∀C:half_ordered_set.