Eunoia is an emerging logical framework for specifying the
proofs and proof systems of SMT solvers, namely CVC5. We present a
translation from Eunoia to the λΠ-calculus modulo rewriting as implemented
by the LambdaPi proof assistant. The translation is implemented by our
tool eo2lp, which we use for generating LambdaPi encodings of (a) a large
fragment of CVC5’s Cooperating Proof Calculus (CPC), and (b) proofs
produced by CVC5 on unsat problems from various fragments of SMT-LIB.
