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