Goal:
    A : Type  P : nat → A → Type  n : nat  l : list A  l' : list A
  ============================
   (Alli P n (l ++ l') → Alli P n l × Alli P (#|l| + n) l')


DEBUG:Going to execute:
induction l in n, l' |- *

Goals:
    A : Type  P : nat → A → Type  n : nat  l' : list A
  ============================
   (Alli P n ([] ++ l') → Alli P n [] × Alli P (#|[]| + n) l')

  
  A : Type
  P : nat → A → Type
  n : nat
  a : A
  l : list A
  l' : list A
  IHl : ∀ (n : nat) (l' : list A),
          Alli P n (l ++ l') → Alli P n l × Alli P (#|l| + n) l'
  ============================
   (Alli P n ((a :: l) ++ l') → Alli P n (a :: l) × Alli P (#|a :: l| + n) l')


DEBUG:Going to execute:
intros H
DEBUG LTAC Evaluated term: l