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 : S n' < S #|l|
  ============================
   (nth_error l n' =
    Some
      (safe_nth l
         (exist (λ n : nat, n < #|l|) n'
            (Arith_base.gt_le_S_stt n' #|l|
               (Arith_base.gt_S_le_stt (S n') #|l| isdecl)))))


DEBUG:Going to execute:
rewrite <- IHl