Is there an already existing plugin to automatically derive, from an Inductive type or predicate, a version of it enriched with the depth/size of the tree? For example, if I have
Inductive Has0 A : list A -> Prop := | Has0_head : forall L, Has0 (0 :: L) | Has0_tail : forall x L, Has0 L -> Has0 (x :: L).
Then I would like to automatically derive another Inductive looking like
Inductive Has0_sized A : list A -> nat -> Prop := | Has0_head_sized : forall L, Has0_sized (0 :: L) 0 | Has0_tail_sized : forall x L n, Has0_sized L n -> Has0_sized (x :: L) (S n).
As well as a lemma of the form
Lemma Has0_sized_of_unsized : forall A (L: list A), Has0 L -> exists n, Has0_sized L n.
If no such plugin exists but someone knows of some code achieving something similar I could take a look at and maybe adapt, it would also be of great help to me.