sig
  type config = Config.config
  type bound = Bound.bound
  type literal = Term.literal
  type clause = Term.clause
  type state = State.state
  type context = Context.context
  type choice_point = State.choice_point
  type explanation = State.explanation
  type propositional_lemmas
  type raw_context_unifier = Context_unifier.raw_context_unifier
  type candidates = Selection_assert.candidates
  type selected = Selection_types.selected
  type space_registry = Context_unifier_space.space_registry
  type lemmas_propositional
  val create :
    Lemma_propositional.config ->
    Lemma_propositional.state ->
    Lemma_propositional.context ->
    Lemma_propositional.candidates ->
    (Lemma_propositional.raw_context_unifier -> unit) ->
    (Lemma_propositional.raw_context_unifier -> bool) ->
    Lemma_propositional.space_registry ->
    Lemma_propositional.lemmas_propositional
  val add_lemma :
    Lemma_propositional.lemmas_propositional ->
    Lemma_propositional.clause -> bool -> unit
  val extend_context :
    Lemma_propositional.lemmas_propositional -> Context.element -> unit
  val get_lemmas :
    Lemma_propositional.lemmas_propositional ->
    Lemma_propositional.clause list
  val backtrack : Lemma_propositional.lemmas_propositional -> unit
end