After merging #234 two files still unfortunately imports `Coq.Init.Logic`: - Initiality/Interpretation.v - TypeCat/General.v It's currently unclear to me if it's easy to fix or requires a more involved patch, so I'm creating this issue both as a reminder and an invitation to anyone who feels inspired to give it a try. Most fixes related to removing `Coq.Init.Logic` has been replacing `trivial` or `auto` with `try apply idpath`, but if you're (un?)lucky you get one of the rare cases where a rewrite is performed using `eq_refl` and then all bets are off.