Inductive GenericTuple : (list Type) -> Type :=
| t_cons : forall (ts:list Type) (T:Type), T -> GenericTuple ts -> GenericTuple (T::ts)
| t_nil : GenericTuple nil.

Implicit Arguments t_cons [ts T].

Check (t_cons 5 (t_cons true (t_cons (2 = 5) t_nil))).

(*
t_cons 5 (t_cons true (t_cons (2 = 5) t_nil))
     : GenericTuple (nat :: (bool :: Prop :: nil)%list)
*)