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


DEBUG:Going to execute:
induction l using rev_ind

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

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


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: rev_ind
DEBUG LTAC Evaluated term: l