CofThy.Disj
type t = disj_thy
val empty : t
val consistency : t -> [ `Consistent | `Inconsistent ]
val assume : t -> cof list -> t
val test_sequent : t -> cof list -> cof -> bool
val envelope_alg : Alg.t -> t
val decompose : t -> Alg.t list
val simplify_cof : t -> cof -> cof
val forall_cof : t -> (Dim.t * cof) -> cof
val meet2 : t -> t -> t