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
  ============================
   (alli p (S (n + k)) l = alli (λ i : nat, p (n + i)) (S k) l)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2