Goal:
  
  A : Type
  P : nat → A → Type
  n : nat
  l : list A
  H : ∀ (n : nat) (x : A), P n x
  ============================
   (Alli P n l)


DEBUG:Going to execute:
induction l in n |- *; constructor