fact: Definition _mk_option_pred {A : Type'} (r : recspace A) : option A -> Prop := fun o => _dest_option o = r.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance