...

[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..f84b740441602122456119aa101139489fb58c86 100644 (file)
--- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
@@ -27,6 +27,7 @@ coercion hint1 nocomposites.
    
 alias symbol "pi1" = "exT \fst".
 alias symbol "N" = "ordered set N".
+alias symbol "dependent_pair" = "dependent pair".
 lemma increasing_supremum_stabilizes:
   ∀sg:‡ℕ.∀a:sequence {[sg]}.
    a is_increasing → 
@@ -58,7 +59,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);]
@@ -98,6 +99,7 @@ letin m ≝ (hide ? (
                 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
                 apply (le_plus ???? (le_n ?) H9);]]]]
 clearbody m; unfold spec in m; clear spec;
+alias symbol "exists" = "CProp exists".
 letin find ≝ (
  let rec find i u on u : nat ≝
   match u with