val size : t -> int
(** Syntactic size of the formula *)
+val eval_form : (StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *)
+
+val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form S1 S2 F] infers S1; S2 |- F *)
+
val print : Format.formatter -> t -> unit
(** Pretty printer *)