fact: Definition _dest_option : forall {A : Type'}, option A -> recspace A := fun A o => match o with | None => @CONSTR A (NUMERAL 0) (@ε A (fun v => True)) (fun _ => @BOTTOM A) | Some a => (fun a' : A => @CONSTR A (S (NUMERAL 0)) a' (fun _ => @BOTTOM A)) a end.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance