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' = nth_error l n')


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| reflexivity
| symmetry; trivial
| contradiction
| congruence ]