Goal:
    A : Type
  ============================
   (∀ l : list A,
      0 < #|l| → nth_error l 0 = nth_error (List.rev l) (#|l| - 1))


DEBUG:Going to execute:
destruct l

Goals:
    A : Type
  ============================
   (0 < #|[]| → nth_error [] 0 = nth_error (List.rev []) (#|[]| - 1))

    A : Type  a : A  l : list A
  ============================
   (0 < #|a :: l|
    → nth_error (a :: l) 0 = nth_error (List.rev (a :: l)) (#|a :: l| - 1))


DEBUG:Going to execute:
simpl

Goals:
    A : Type
  ============================
   (0 < 0 → None = None)

    A : Type  a : A  l : list A
  ============================
   (0 < S #|l| → Some a = nth_error (List.rev l ++ [a]) (#|l| - 0))


DEBUG:Going to execute:
auto

Goals:
    A : Type
  ============================
   (0 < 0 → None = None)

    A : Type  a : A  l : list A
  ============================
   (0 < S #|l| → Some a = nth_error (List.rev l ++ [a]) (#|l| - 0))


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