Goal:
    A : Type  B : Type  P : B → Type  f : nat → A → B  l : list A  k : nat
  ============================
   (Alli (λ (i : nat) (x : A), P (f i x)) k l → All P (mapi_rec f l k))


DEBUG:Going to execute:
induction 1; simpl