Goal:
  
  A : Type
  B : Type
  C : Type
  g : nat → A → B
  f : nat → B → C
  a : A
  l : list A
  IHl : ∀ n : nat,
          mapi_rec f (mapi_rec g l n) n =
          mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) l n
  ============================
   (∀ n : nat,
      f n (g n a) :: mapi_rec f (mapi_rec g l (S n)) (S n) =
      f n (g n a) :: mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) l (S n))


DEBUG:Going to execute:
congruence