sig
  type state = State.state
  type choice_point = State.choice_point
  type context = Context.context
  type literal = Term.literal
  type clause = Term.clause
  type subst = Subst.subst
  val get_lemma :
    uip:bool ->
    Lemma_grounded.state ->
    Lemma_grounded.context ->
    Lemma_grounded.subst ->
    Lemma_grounded.clause ->
    Lemma_grounded.literal array ->
    Lemma_grounded.choice_point -> Lemma_grounded.clause option
end