Verification performance drop with typeclasses

[hacklex]

Verification proceeds really slowly when the typeclass tree is step or two above trivial...

See my ringlike algebraic structures, dependencies are

• FStar.Algebra.Classes.Equatable
• FStar.Algebra.Classes.Grouplike from the same repository (no need to clone it entirely).

Problematic are line 314 and the very last lemma.

Uncommenting additional (redundant!) instance definitions helps a bit. But the last lemma still takes too much time to verify for some reason.

Perhaps this is something that might get fixed with caching previously resolved typeclass instances...