Goal:
  
  A : Type
  n : nat
  k : nat
  p : nat → A → bool
  a : A
  l : list A
  IHl : ∀ (n k : nat) (p : nat → A → bool),
          alli p (n + k) l = alli (λ i : nat, p (n + i)) k l
  ============================
   (p (n + k) a && alli p (S (n + k)) l =
    p (n + k) a && alli (λ i : nat, p (n + i)) (S k) l)


DEBUG:Going to execute:
f_equal