X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Flist_utility.ma;h=1c062a91297894d71284e594a553aa880a0c82e7;hb=f8d45b2e4fa7817d7ef8312b3bb8a7439bd7fb8c;hp=3ffd1d3c5df48cd6f91116570aa2b1f7cc3c45ca;hpb=3819ff5482f28f3bb9be822513c7bd73c47a46e0;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index 3ffd1d3c5..1c062a912 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -188,7 +188,7 @@ nlet rec abs_list (T:Type) (l:list T) on l ≝
 
 (* listlen *)
 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
- match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
+ match nl with [ ne_nil _ ⇒ (S O) | ne_cons _ t ⇒ S (len_neList T t) ].
 
 (* reverse *)
 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
@@ -321,8 +321,6 @@ ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) >
 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
 
-naxiom daemon : False.
-
 nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
  match l
   return λl.Πn.(((len_neList T l) > n) = true) → T