exception Not_a_th_term
val id_and : Sidekick_base.ID.tval id_or : Sidekick_base.ID.tval id_imply : Sidekick_base.ID.tval view_id : Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> ('a, 'a Sidekick_util.IArray.iter) Sidekick_th_bool_static.bool_viewval view_as_bool : T.t -> (T.t, T.t Sidekick_util.IArray.iter) Sidekick_th_bool_static.bool_view
module Funs : sig ... endval as_id : Sidekick_base.ID.t -> T.t -> T.t Sidekick_util.IArray.t optionval flatten_id : Sidekick_base.ID.t -> bool -> T.t list -> T.t listval and_l : T.store -> T.t list -> T.tval or_l : T.store -> T.t list -> T.tval and_ : T.store -> T.t -> T.t -> T.tval or_ : T.store -> T.t -> T.t -> T.tval and_a : T.store -> T.t Sidekick_util.IArray.t -> T.tval or_a : T.store -> T.t Sidekick_util.IArray.t -> T.tval eq : T.store -> T.t -> T.t -> T.tval not_ : T.store -> T.t -> T.tval ite : T.store -> T.t -> T.t -> T.t -> T.tval equiv : T.store -> T.t -> T.t -> T.tval neq : T.store -> T.t -> T.t -> T.tval imply_a : T.store -> T.t Sidekick_util.IArray.t -> T.t -> T.tval imply_l : T.store -> T.t list -> T.t -> T.tval imply : T.store -> T.t -> T.t -> T.tval xor : T.store -> T.t -> T.t -> T.tval distinct_l : T.store -> T.t CCList.t -> T.tval mk_bool : T.store -> (T.t, T.t Sidekick_util.IArray.t) Sidekick_th_bool_static.bool_view -> T.t
val check_congruence_classes : bool