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


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrtclby@0> $1