Goal:
  
  A : Type
  P : A → Prop
  a : A
  x : A
  a0 : A
  l : list A
  H : x :: a0 :: l ≠ []
  H0 : P x
  H1 : Forall P (a0 :: l)
  IHForall : a0 :: l ≠ [] → P (last (a0 :: l) a)
  ============================
   (a0 :: l ≠ [])


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1
DEBUG LTAC Evaluated term: IHForall