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 < #|args|
  ============================
   (n < Nat.pred #|args|)


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