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


DEBUG:Going to execute:
f_equal