IncrementalUnfolding.Make
module Encoding : Translation_sig.ENCODING
module Solver : Backend_sig.BACKEND
val unfold : Context.t -> SMT.t -> SL.t -> SL.t