Goal:
  
  A : Type
  a : A
  args : list A
  n : nat
  IHn : ∀ args : list A,
          n < Nat.pred #|args|
          → nth_error args n = nth_error (removelast args) n
  H : S n < Nat.pred #|a :: args|
  ============================
   (nth_error (removelast args) n =
    match
      match args with
      | [] => []
      | _ :: _ => a :: removelast args
      end
    with
    | [] => None
    | _ :: l => nth_error l n
    end)


DEBUG:Going to execute:
destruct args, n

Goals:
  
  A : Type
  a : A
  IHn : ∀ args : list A,
          0 < Nat.pred #|args|
          → nth_error args 0 = nth_error (removelast args) 0
  H : 1 < Nat.pred #|[a]|
  ============================
   (nth_error (removelast []) 0 = None)

  
  A : Type
  a : A
  n : nat
  IHn : ∀ args : list A,
          S n < Nat.pred #|args|
          → nth_error args (S n) = nth_error (removelast args) (S n)
  H : S (S n) < Nat.pred #|[a]|
  ============================
   (nth_error (removelast []) (S n) = None)

  
  A : Type
  a : A
  a0 : A
  args : list A
  IHn : ∀ args : list A,
          0 < Nat.pred #|args|
          → nth_error args 0 = nth_error (removelast args) 0
  H : 1 < Nat.pred #|a :: a0 :: args|
  ============================
   (nth_error (removelast (a0 :: args)) 0 =
    nth_error (removelast (a0 :: args)) 0)

  
  A : Type
  a : A
  a0 : A
  args : list A
  n : nat
  IHn : ∀ args : list A,
          S n < Nat.pred #|args|
          → nth_error args (S n) = nth_error (removelast args) (S n)
  H : S (S n) < Nat.pred #|a :: a0 :: args|
  ============================
   (nth_error (removelast (a0 :: args)) (S n) =
    nth_error (removelast (a0 :: args)) (S n))


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

Goals:
  
  A : Type
  a : A
  IHn : ∀ args : list A,
          0 < Nat.pred #|args|
          → nth_error args 0 = nth_error (removelast args) 0
  H : 1 < Nat.pred #|[a]|
  ============================
   (nth_error (removelast []) 0 = None)

  
  A : Type
  a : A
  n : nat
  IHn : ∀ args : list A,
          S n < Nat.pred #|args|
          → nth_error args (S n) = nth_error (removelast args) (S n)
  H : S (S n) < Nat.pred #|[a]|
  ============================
   (nth_error (removelast []) (S n) = None)

  
  A : Type
  a : A
  a0 : A
  args : list A
  IHn : ∀ args : list A,
          0 < Nat.pred #|args|
          → nth_error args 0 = nth_error (removelast args) 0
  H : 1 < Nat.pred #|a :: a0 :: args|
  ============================
   (nth_error (removelast (a0 :: args)) 0 =
    nth_error (removelast (a0 :: args)) 0)

  
  A : Type
  a : A
  a0 : A
  args : list A
  n : nat
  IHn : ∀ args : list A,
          S n < Nat.pred #|args|
          → nth_error args (S n) = nth_error (removelast args) (S n)
  H : S (S n) < Nat.pred #|a :: a0 :: args|
  ============================
   (nth_error (removelast (a0 :: args)) (S n) =
    nth_error (removelast (a0 :: args)) (S n))


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