Goal:
  
  A : Type
  P : nat → A → Type
  k : nat
  a : A
  l : list A
  n : nat
  IHl : ∀ k n : nat, Alli P (n + k) l → Alli (λ x : nat, P (n + x)) k l
  X : Alli P (n + k) (a :: l)
  ============================
   (P (n + k) a)


DEBUG:Going to execute:
fun H => inversion_clear H