...

[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 46aa96eb1c141b1a0a29554efdfc4157104dd913..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 → 
@@ -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