sig
  type literal = Term.literal
  val close_literal : Lemma.literal
  val simplify : Lemma.literal list list -> Lemma.literal list
end