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 |- *; destruct args; intros