The Coq mailing list

[Venanzio Capretta <venanzio AT cs.ru.nl>]

Here is a solution. I'm not sure it is better than yours: it just hides 
the ugly parts (to do with inversions) into a couple of auxiliary 
functions (definitions below):
 bound_0_elim: forall A:Type, (Bounded 0) -> A
 bounded_zero_succ: forall (n:nat)(i:Bounded (S n)),
                    {j:Bounded n | i = Succ j} + {i=Zero n}.

But at least you can define prefix in a shorter and more intuitive way:

Definition prefix: forall (A:Set)(n:nat)(i:Bounded (S n)),
 vector A n -> vector A (Bounded_to_nat i).
induction 1.
case (bounded_zero_succ 0 i).
 intros [j Hij]; apply bound_0_elim with (1:=j).
 intros Hi; rewrite Hi; exact (Vnil A).
case (bounded_zero_succ (S n) i).
 intros [j Hij]; rewrite Hij; simpl.
 apply Vcons.
 exact a.
 exact (IHvector j).
 intro Hi; rewrite Hi; exact (Vnil A).
Defined.

where we have defined:

Definition bound_0_elim_type (n:nat)(A:Type): Type :=
match n with
 0 => A
| (S n) => unit
end.

Definition bound_0_elim_aux (n:nat)(A:Type)(i:Bounded n): 
bound_0_elim_type n A:=
match i in (Bounded n) return (bound_0_elim_type n A) with
 (Zero n) => tt
| (Succ n i) => tt
end.

Definition bound_0_elim: forall A:Type, (Bounded 0) -> A :=
fun A i => bound_0_elim_aux 0 A i.

Definition bounded_zero_succ:
 forall (n:nat)(i:Bounded (S n)),
   {j:Bounded n | i = Succ j} + {i=Zero n}.
set
(P:= fun m =>
    match m return Bounded m -> Set with
      O => fun _ => unit
    | S n => fun i => {j:Bounded n | i = Succ j} + {i=Zero n}
    end).
intros n i; change (P (S n) i).
cut (forall m i, P m i).
intros H; apply H.
clear n i; intros m i; elim i.
intro n; simpl; auto.
intros n j IH; simpl.
left.
exists j.
trivial.
Defined.