I have defined an inductive definition of lists (called listkind
) in order make it easy
for me to prove a specific theorem by induction on listkind
rather than on list.
Inductive listkind {X}: list X -> Prop :=
| l_nil : listkind []
| l_one : forall a:X, listkind [a]
| l_app : forall l, listkind l -> forall a b, listkind ([a]++l++[b]).
(With this property, to prove things about lists, I have to prove the cases where a list is [], [a], or [a]++l++[b], rather than the cases where a list is [] or a::l. In my particular theorem, those cases fit better and makes the proof simpler.)
However, to be able to use listkind in my proof, I have to prove
Lemma all_lists_are_listkind: (forall {X} (l:list X), listkind l).
Having tried various approaches, I find myself stuck at this point. I would very much appreciate seeing how to perform such a proof, preferably with minimal coq magic applied.