maction support added to notation, adopted for = AKA = \sub t

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

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 6dc55e1426ae332f77ad84c4c88542d70cf150ec..46aa96eb1c141b1a0a29554efdfc4157104dd913 100644 (file)
--- 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);]