fact: Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } := match mx return { x | mx = Some x } + { mx = None } with | Some x => inleft (x ↾ eq_refl _) | None => inright eq_refl end.
imports: stdpp(options)