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


DEBUG:Going to execute:
induction l

Goals:
    A : Type
  ============================
   (∀ (n : nat) (isdecl : n < #|[]|),
      nth_error [] n =
      Some (safe_nth [] (exist (λ n0 : nat, n0 < #|[]|) n 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 : n < #|a :: l|),
      nth_error (a :: l) n =
      Some (safe_nth (a :: l) (exist (λ n0 : nat, n0 < #|a :: l|) n isdecl)))


DEBUG:Going to execute:
intros
DEBUG LTAC Evaluated term: l