Goal:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  d : D
  l' : list D
  IHl : ∀ (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'
  n : nat
  ============================
   (f n (g a d) :: mapi_rec f (map2 g l l') (S n) =
    f n (g a d)
    :: map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) (S n) l l')


DEBUG:Going to execute:
f_equal