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))
  isdecl : 0 < #|a :: l|
  ============================
   (Some a = Some a)


DEBUG:Going to execute:
reflexivity