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