Goal:
  
  A : Type
  B : Type
  P : nat → B → Type
  f : nat → A → B
  k : nat
  l : list A
  ============================
   (Alli (λ (n : nat) (a : A), P n (f n a)) k l <~> Alli P k (mapi_rec f l k))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>