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
  H : k0 ≤ k
  ============================
   (mapi_rec f l (S k0) = mapi_rec g l (S k0))


DEBUG:Going to execute:
eapply (IHl (S k))

Goals:
  
  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
  H : k0 ≤ k
  ============================
   (∀ (k' : nat) (x : A), k' < S k + #|l| → f k' x = g k' x)

  
  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
  H : k0 ≤ k
  ============================
   (S k0 ≤ S k)


DEBUG:Going to execute:
try lia
DEBUG LTAC Evaluated term: (IHl (S k))