X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fincreasing_supremum_stabilizes.ma;h=58626ff158f194d539a471339a86ac09db1f4db5;hb=7a9277a3775b7150a22b2039548508e85751f85a;hp=9a43d186df269707aee4134ba69ed2dc15569923;hpb=a6f88a0acfcb5c5284b7b3781e313cc0f76bb76d;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma
index 9a43d186d..58626ff15 100644
--- a/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma
@@ -59,7 +59,7 @@ letin m ≝ (hide ? (
         [2: cases Hx; lapply (os_le_to_nat_le ?? H1);
             apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
         |1: intros; unfold Type_of_ordered_set in sg;
-            lapply (H2 O) as K; lapply (sl2l ?? (a O) ≪x,Hx≫ K) as P;
+            lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
             simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
             lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
     |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n];