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 67209928116df8aec54e7a70e5304a0011d257e1..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