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


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