In these files, one or more lemmas that are used (along with eauto) silently ties the results of the lemma to specific definitions of the typeclass instances.
These is bad design in my opinion. Such proofs will become hard to maintain and change.
The code is also not readable to developers.
We need to find a better way of handling these tyepclass instances.
In our concrete case, I don't think it make sense to put the nontypeclass parameters inside typeclasses.
Then we can either make it a rule to state definitions with nontypeclass parameters fed at the top of file or explore using canonical instances instead of typeclasses