Coq’s trusted codebase (TCB) is currently nearly 30,000 lines of OCaml. We propose to shrink this TCB by translating Coq developments to Cedille, a theorem prover which has a TCB thirty times smaller. Since both theorem provers are based on the Calculus of Constructors, this translation is rather straightforward, however there are still two key mismatches, viz.: Disjointnes of Datatype Constructors; and Type Equivalences. This abstract presents our approach to bridging this gap. As a proof of concept, we are currently implementing Coquedille, a Coq to Cedille transpiler written in Coq.