X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=a492c8f3299e8255c0b86be2605972da857b3310;hb=591ffe6f23ec9d2a4d368d2c1e7b213986189e44;hp=a48eb164a822af5044ad648632000895b3557bbc;hpb=ca41435a6021292ccba239aa173651c0be705b45;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index a48eb164a..a492c8f32 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -217,7 +217,7 @@ qed.
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
    exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
-     (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
+     (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).
     
 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45