Draft: Avoid making definitions from stdlib type class transparent
See the discussion here: #Rocq users > Trouble with two libraries interracting. The fact that we made these instances transparent, makes it hard to combine different libraries.
I tried to undo these side effects. The impact is relatively minor:
- Some "derived"
Injinstances relied oncomposebeing transparent. That should be super easy to fix. - In the instance
id_inj, Rocq somehow unfoldsidwhen written as@id A. I don't understand this. But writingidinstead of@idsolves it... - The lemma
list_find_fmapstatement does not type check because it cannot find aDecisionbecausecomposeis no longer unfolded. Perhaps we need aHint Externhere.