(* 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 ≝
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