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


DEBUG:Going to execute:
idtac