type formula = Atom of string | Neg of formula | And of formula * formula | Or of formula * formula | Prog of int * formula | Mu of (string * formula) list * string | Var of string | True exception Freevar of string val replace : (string * formula) list -> formula -> formula val print : formula -> unit val lean : formula -> int * (Bf.af * int) list * Bf.t val plunge : formula -> formula val compress : formula -> (formula* (string list -> string)) val testfreevar : formula -> formula