Goal:
    A : Type  B : Type  P : nat → B → Type  f : nat → A → B  k : nat
  ============================
   (Alli P k [] → Alli (λ (n : nat) (a : A), P n (f n a)) k [])


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>
DEBUG LTAC Evaluated term: l