X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fmodels%2Fincreasing_supremum_stabilizes.ma;h=46aa96eb1c141b1a0a29554efdfc4157104dd913;hb=8d961585c4ff785d558d5b4c84adf656595ca487;hp=6dc55e1426ae332f77ad84c4c88542d70cf150ec;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git

diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
index 6dc55e142..46aa96eb1 100644
--- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
@@ -58,7 +58,7 @@ letin m ≝ (hide ? (
         rewrite > (?:x = O); 
         [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;
+        |1: intros; unfold Type_OF_ordered_set in sg a; whd in a:(? %);
             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);]