Goal:
    A : Type  B : Type  f : nat → A → bool  g : nat → B → A  l : list B
  ============================
   (∀ n : nat,
      alli f n (mapi_rec g l n) = alli (λ (i : nat) (x : B), f i (g i x)) n l)


DEBUG:Going to execute:
induction l => n