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


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrtclintros@0> arg
DEBUG LTAC Evaluated term: (IHl (S n) k p)
DEBUG LTAC Evaluated term: (IHl (S n) k p)
DEBUG LTAC Evaluated term: (IHl 1 k ?p)
DEBUG LTAC Evaluated term: (IHl 1 k ?p)