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 args n =
    match
      match args with
      | [] => []
      | _ :: _ => a :: removelast args
      end
    with
    | [] => None
    | _ :: l => nth_error l n
    end)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2