X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fproperty_exhaustivity.ma;h=deddf88049f5e60a2108942506b67a65bf79bf80;hb=179574c117d34a39cebeaa66673cda83974e135a;hp=7145b42886c802cc4d75574a77e3c64906e357ea;hpb=bb7af347df386afcd3ea2adea8e7e982e3a5a253;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 7145b4288..deddf8804 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -35,11 +35,11 @@ lemma h_segment_preserves_uparrow:
   ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
    ∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
 intros; cases H (Ha Hx); split;
-[ intro n; intro H; apply (Ha n); apply (sx2x ???? H);
+[ intro n; intro H; apply (Ha n); apply rule H;
 | cases Hx; split; 
-  [ intro n; intro H; apply (H1 n);apply (sx2x ???? H); 
-  | intros; cases (H2 (\fst y)); [2: apply (sx2x ???? H3);] 
-    exists [apply w] apply (x2sx ?? (a w) y H4);]]
+  [ intro n; intro H; apply (H1 n);apply rule H; 
+  | intros; cases (H2 (\fst y)); [2: apply rule H3;] 
+    exists [apply w] apply (x2sx_ ?? (a w) y H4);]]
 qed.
 
 notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.