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


DEBUG:Going to execute:
revert n isdecl; induction l