...

[helm.git] / helm / software / matita / contribs / dama / dama / property_exhaustivity.ma

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 7145b42886c802cc4d75574a77e3c64906e357ea..deddf88049f5e60a2108942506b67a65bf79bf80 100644 (file)
--- 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}.