val ( >=> ) : state*(TagSet.t*bool*predicate) -> formula -> t
val ( +| ) : formula -> formula -> formula
val ( *& ) : formula -> formula -> formula
val ( >=> ) : state*(TagSet.t*bool*predicate) -> formula -> t
val ( +| ) : formula -> formula -> formula
val ( *& ) : formula -> formula -> formula