Goal:
    A : Type  B : Type  f : nat → A → B  n : nat  k : nat
  ============================
   (nth_error (mapi_rec f [] k) n = option_map (f (n + k)) (nth_error [] n))


DEBUG:Going to execute:
destruct n
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  B : Type  f : nat → A → B  k : nat
  ============================
   (nth_error (mapi_rec f [] k) 0 = option_map (f (0 + k)) (nth_error [] 0))

    A : Type  B : Type  f : nat → A → B  n : nat  k : nat
  ============================
   (nth_error (mapi_rec f [] k) (S n) =
    option_map (f (S n + k)) (nth_error [] (S n)))


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: n

Goals:
    A : Type  B : Type  f : nat → A → B  k : nat
  ============================
   (nth_error (mapi_rec f [] k) 0 = option_map (f (0 + k)) (nth_error [] 0))

    A : Type  B : Type  f : nat → A → B  n : nat  k : nat
  ============================
   (nth_error (mapi_rec f [] k) (S n) =
    option_map (f (S n + k)) (nth_error [] (S n)))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>