Remove dependency on Coq.Init.Logic

[m-lindgren]

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.

[Skantz]

Hi,

I tried to remove the import from the last two files: https://gist.github.com/Skantz/52047f07f044846b0af2774b981d10c7

If it looks good, I am happy to submit the PR.

[benediktahrens]

@Skantz : that's great, thanks a lot! It definitely looks good.