freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / common / list_utility.ma

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 ce118e74c11af46c24c08ef6efd7f9d7770d26a1..1c062a91297894d71284e594a553aa880a0c82e7 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -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