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