Goal:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  l : list C
  l' : list D
  ============================
   (∀ n : nat,
      mapi_rec f (map2 g l l') n =
      map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l')


DEBUG:Going to execute:
induction l in l' |- *; intros