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:
symmetry