Goal:
    z : t  hd : A.t  tl : list A.t
  ============================
   (lt (hd :: tl) z -> lt [] z)


DEBUG:Going to execute:
intros H; depelim H