importing Finset breaks deriving DecidableEq

Stream: new members

[Malvin Gattinger]

I moved to lean 4.2.0-rc4 in order to use deriving DecidableEq for mutually inductive types, but now run into this.

I want to use Finset in the same file.

[Malvin Gattinger]

(Related previous discussion at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/induction.20for.20mutually.20inductive.20types/near/395084790 )