Goal:
  
  A : Type
  B : Type
  f : nat → A → B
  g : nat → A → B
  a : A
  l : list A
  k : nat
  Hl : ∀ (k' : nat) (x : A), k' < k + S #|l| → f k' x = g k' x
  IHl : ∀ k : nat,
          (∀ (k' : nat) (x : A), k' < k + #|l| → f k' x = g k' x)
          → ∀ k0 : nat, k0 ≤ k → mapi_rec f l k0 = mapi_rec g l k0
  k0 : nat
  k' : nat
  x : A
  H0 : BinInt.Z.lt (BinInt.Z.of_nat k')
         (BinInt.Z.add
            (BinInt.Z.add (BinInt.Z.of_nat k) (BinNums.Zpos BinNums.xH))
            (BinInt.Z.of_nat #|l|))
  H : BinInt.Z.le (BinInt.Z.of_nat k0) (BinInt.Z.of_nat k)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat k)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat k0)
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  cstr2 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat k')
  ============================
   (f k' x = g k' x)


DEBUG:Going to execute:
constr:(false)