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


DEBUG:Going to execute:
induction l in l' |- *; destruct l'; simpl
DEBUG LTAC Evaluated term: IHl
DEBUG LTAC Evaluated term: 0