Require Import Vector.

Inductive Vector_In2 {A : Type} (a : A) : forall {n}, t A n -> Type :=
| vec_inB {n} (v : t A n) : Vector_In2 a (cons A a n v)
| vec_inS a' {n} (v : t A n) : Vector_In2 a v -> Vector_In2 a (cons A a' n v).
#[global] Hint Constructors Vector_In2 : core.