let close_literal =
  Term.request_literal
    true
    (Term.request_const Symbol.lemma_root)