WIP

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

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 1dba15a7c00242c47bccee31ea638411660af3bf..36ba2d287503736707f4911fe6407d6fcee08d27 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -202,7 +202,7 @@ intros (O s); apply mk_ordered_uniform_space;
 ]  
 qed.
 
-interpretation "Ordered uniform space segment" 'segment_set a = 
+interpretation "Ordered uniform space segment" 'segset a = 
  (segment_ordered_uniform_space _ a).
 
 (* Lemma 3.2 *)
@@ -210,7 +210,7 @@ alias symbol "pi1" = "exT \fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀s:‡O.
   ∀x:{[s]}.
-   ∀a:sequence (segment_ordered_uniform_space O s).
+   ∀a:sequence {[s]}.
     (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) → 
       a uniform_converges x.
 intros 7; cases H1; cases H2; clear H2 H1;