fact: Definition vhd'' {A:Type}{n:nat}(v : t A n) : n <> 0 -> A := match v in t _ n return (n <> 0 -> A) with | nil _ => (fun h : 0<> 0 => False_rect A (absurd_positive h)) | cons _ a _ w => fun h => a end.
imports: Vector