Abstract Eunoia is a logical framework designed for specifying the proofs and proof systems of SMT solvers, namely cvc5 . We present a translation from a core fragment of Eunoia to the $$\lambda \Pi $$ λ Π -calculus modulo rewriting as implemented by the LambdaPi proof assistant. The translation is implemented by our tool , which we use for generating LambdaPi encodings of (a) a large fragment of the Cooperating Proof Calculus (CPC), the Eunoia signature defining cvc5 ’s proof system, and (b) proofs produced by cvc5 on problems from various fragments of SMT-LIB.