some more work

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

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index ba90bb0ab50097e864bdf9c884902aa049098c44..2e0e73bc6edc3c08f10767adc737d38d3150373e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -63,7 +63,7 @@ lemma sigma_cauchy:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
 intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
-alias symbol "pair" = "pair".
+alias symbol "pair" = "Pair construction".
 letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   match i with
@@ -77,9 +77,8 @@ letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
       intros; lapply (H5 i j) as H14;
         [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
       cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
-      generalize in match H6; generalize in match H7;
-      cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
-      apply H12; [3: apply le_S_S_to_le; assumption]
+      cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+      apply H6; [3: apply le_S_S_to_le; assumption]
       apply lt_to_le; apply (max_le_r w1); assumption;
   |4: intros; clear H6; rewrite > H4 in H5; 
       rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;]