Here is a solution:
Require Import List Omega.
Lemma all_lists_are_listkind_size: forall {X} (n:nat) (l:list X), length l <= n -> listkind l.
Proof.
intros X.
induction n as [ | n hi]; simpl in *; intros l hl.
- destruct l as [ | hd tl]; simpl in *.
+ now constructor.
+ now inversion hl.
- destruct l as [ | hd tl]; simpl in *.
+ now constructor.
+ induction tl using rev_ind.
* now constructor.
* constructor.
apply hi.
rewrite app_length in hl; simpl in hl.
omega. (* a bit overkill but it does the arithmetic job *)
Qed.
Lemma all_lists_are_listkind: forall {X} (l:list X), listkind l.
Proof.
intros.
apply all_lists_are_listkind_size with (length l).
apply le_refl.
Qed.
The main idea is that your lists have the same size as regular list, and induction on a natural is goes more smoothly than induction on a non trivial shape of list.
Hope it helps, V.