Goal:
    A : Type  args : list A  n : nat
  ============================
   (n < Nat.pred #|args| → nth_error args n = nth_error (removelast args) n)


DEBUG:Going to execute:
induction n in args |- *

Goals:
    A : Type  args : list A
  ============================
   (0 < Nat.pred #|args| → nth_error args 0 = nth_error (removelast args) 0)

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


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

Goals:
    A : Type
  ============================
   (0 < Nat.pred #|[]| → nth_error [] 0 = nth_error (removelast []) 0)

    A : Type  a : A  args : list A
  ============================
   (0 < Nat.pred #|a :: args|
    → nth_error (a :: args) 0 = nth_error (removelast (a :: args)) 0)

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

  
  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
  ============================
   (S n < Nat.pred #|a :: args|
    → nth_error (a :: args) (S n) = nth_error (removelast (a :: args)) (S n))


DEBUG:Going to execute:
intros
DEBUG LTAC Evaluated term: args
DEBUG LTAC Evaluated term: args

Goals:
    A : Type  H : 0 < Nat.pred #|[]|
  ============================
   (nth_error [] 0 = nth_error (removelast []) 0)

    A : Type  a : A  args : list A  H : 0 < Nat.pred #|a :: args|
  ============================
   (nth_error (a :: args) 0 = nth_error (removelast (a :: args)) 0)

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

  
  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 (a :: args) (S n) = nth_error (removelast (a :: args)) (S n))


DEBUG:Going to execute:
auto

Goals:
    A : Type  H : 0 < Nat.pred #|[]|
  ============================
   (nth_error [] 0 = nth_error (removelast []) 0)

    A : Type  a : A  args : list A  H : 0 < Nat.pred #|a :: args|
  ============================
   (nth_error (a :: args) 0 = nth_error (removelast (a :: args)) 0)

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

  
  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 (a :: args) (S n) = nth_error (removelast (a :: args)) (S n))


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3