Prevent [finite_countable] from solving unrelated evars

Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw. Fixes #160 (closed).

The problem is that Hint Immediate translates to (something like) simple apply @finite.finite_countable ; trivial in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.

Missing (I assume):

• trivial only uses hints with cost 0, but typeclasses eauto 0 does not appear to work, so typeclasses eauto 1 is the closest thing I see. This might be a problem.
• Testcase
• Changelog? Probably not needed since this is a bugfix
• Mention this in upstream issue.

Also see Coq issue https://github.com/coq/coq/issues/16893.