Goal:
  
  A : Type
  a : A
  l : list A
  IHl : ∀ (n : nat) (isdecl : n < #|l|),
          nth_error l n =
          Some (safe_nth l (exist (λ n0 : nat, n0 < #|l|) n isdecl))
  n : nat
  isdecl : n < #|a :: l|
  ============================
   (nth_error (a :: l) n =
    Some (safe_nth (a :: l) (exist (λ n : nat, n < #|a :: l|) n isdecl)))


DEBUG:Going to execute:
destruct n as [| n']

Goals:
  
  A : Type
  a : A
  l : list A
  IHl : ∀ (n : nat) (isdecl : n < #|l|),
          nth_error l n =
          Some (safe_nth l (exist (λ n0 : nat, n0 < #|l|) n isdecl))
  isdecl : 0 < #|a :: l|
  ============================
   (nth_error (a :: l) 0 =
    Some (safe_nth (a :: l) (exist (λ n : nat, n < #|a :: l|) 0 isdecl)))

  
  A : Type
  a : A
  l : list A
  IHl : ∀ (n : nat) (isdecl : n < #|l|),
          nth_error l n =
          Some (safe_nth l (exist (λ n0 : nat, n0 < #|l|) n isdecl))
  n' : nat
  isdecl : S n' < #|a :: l|
  ============================
   (nth_error (a :: l) (S n') =
    Some (safe_nth (a :: l) (exist (λ n : nat, n < #|a :: l|) (S n') isdecl)))


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: n