fact: Definition asOption (o : option T) (d : Checked o) : option (match o with | None => False | Some x => F x end) := match d in Checked o return option match o with | None => False | Some x => F x end with | Success _ x => Some x | Failure => None end.