(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
val embed : t -> t foterm
(* saturate [proof] [type] -> [proof] * [type] *)
val saturate : t -> t -> t foterm * t foterm
val embed : t -> t foterm
(* saturate [proof] [type] -> [proof] * [type] *)
val saturate : t -> t -> t foterm * t foterm