Goal:
  
  A : Type
  P : nat → A → Type
  n : nat
  x : A
  hd : A
  tl : list A
  n0 : nat
  p : P n0 hd
  HPl : Alli P (S n0) tl
  IHHPl : ∀ n : nat, nth_error tl n = Some x → P (S n0 + n) x
  H' : nth_error (hd :: tl) (S n) = Some x
  ============================
   (P (n0 + S n) x)


DEBUG:Going to execute:
eauto