The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>]

Hi,

yep you have to break the dependance in the equality.
Adam's idea but with tactic:

Lemma openVector: forall A n (v: vector A (S n)),
   exists a, exists v0, v = vcons a v0.
intros A n v.
change
((fun n: nat => match n return vector A n -> Prop with
  O => fun _ => True (* what you want *)
| S n1 => fun v =>
     exists a : A, exists v0 : vector A n1, v = vcons a v0
end) (S n) v).
dependent inversion v as [|n1 a1 v1].
exists a1; exists v1; auto.
Qed.