The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Eric Finster wrote:
> I'm trying to do a case analysis over an inductive type where the
> allowed constructors are restricted by the type of a term.  It
> essentially equivalent to the following setup with indexed lists:
>
> Inductive Vect (A : Type) : nat → Type :=
> | VNil : Vect A 0
> | VCons : forall n : nat, A → Vect A n → Vect A (S n).
>
> Lemma zero_len_is_nil (A : Type) (v : Vect A 0) : v = VNil A.
>    

This precise type family, and some functions and theorems closely 
related to your question, are considered in detail in Chapters 8 and 9 
of CPDT:
    http://adam.chlipala.net/cpdt/