x2sx declared as coercion and used when possible

[helm.git] / helm / software / matita / contribs / dama / dama / models / increasing_supremum_stabilizes.ma

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 9a43d186df269707aee4134ba69ed2dc15569923..58626ff158f194d539a471339a86ac09db1f4db5 100644 (file)
--- 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];