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; simpl
DEBUG LTAC Evaluated term: i