Require Import Vector.
Definition ForallT {X} (p : X -> Type) := fix ForallT {n} (v : t X n) :=
  match v with
  | nil _ => (unit : Type)
  | cons _ x _ v => (p x * ForallT v)%type
  end.