The functions can be used to generate HOL4 level certificates without stepping
out of the logic and calling Daisy. As the functions are not verified their
returned certificate should still be send through the checker pipeline.
The sole benefit of the functions is that they can be used as in-logic
generators for checker input.