open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Jmeq

open Russell

open Bool

open Nat

open List

open Setoids

open Relations

open Monad

val option : Monad.monadProps

val opt_safe : 'a1 Types.option -> 'a1

val opt_try_catch : 'a1 Types.option -> (Types.unit0 -> 'a1) -> 'a1

val optPred : Monad.injMonadPred