SMT.Boolean
include SMT_sig.EQUALITY with type t := t
val mk_eq : t list -> t
val mk_distinct : t list -> t
val mk_var : string -> t
val mk_fresh_var : string -> t
val mk_const : bool -> t
val tt : t
val ff : t
val mk_and : t list -> t
val mk_or : t list -> t
val mk_not : t -> t
val mk_implies : t -> t -> t
val mk_iff : t list -> t
val mk_ite : t -> t -> t -> t
val mk_and2 : t -> t -> t
val mk_or2 : t -> t -> t
val mk_multiple_ite : (t * t) list -> t -> t