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