Goal:
    n : Z
  ============================
   (to_label (Some n) = Z.to_nat n)


DEBUG:Going to execute:
trivial; hnf; intros