Goal:
    A : Type  n : nat  l : list A  d : A
  ============================
   (nth n l d = match nth_error l n with
                | Some x => x
                | None => d
                end)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::symmetry@0>