X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fproperty_sigma.ma;h=e482d79a05985db6cf3cb766698efeb763dbaa01;hb=5bed3ef9523751da77b0c57a85fd880083cde248;hp=74f03de4c9fe2ee552a207c79b15c5413fe85962;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/property_sigma.ma b/helm/software/matita/library/dama/property_sigma.ma
index 74f03de4c..e482d79a0 100644
--- a/helm/software/matita/library/dama/property_sigma.ma
+++ b/helm/software/matita/library/dama/property_sigma.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_uniform.ma".
-include "russell_support.ma".
+include "dama/ordered_uniform.ma".
+include "dama/russell_support.ma".
 
 (* Definition 3.5 *)
 alias num (instance 0) = "natural number".
@@ -108,7 +108,7 @@ lapply (H9 ?? H10) as H11; [
   |7:apply (ge_reflexive (l : hos_carr (os_r C)));
   |8:apply (H12 i);
   |6:change with (a i ≤ a (m O));
-     apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
+     apply (trans_decreasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
 generalize in match (refl_eq nat (m p)); 
 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;