importing finset breaks deriving DecidableEq

Stream: new members

[Malvin Gattinger]

-- import Mathlib.Data.Finset.Basic -- uncomment this ...
-- import Mathlib.Data.Nat.Order.Basic -- or this ...

mutual
inductive Tree : Type :=
  | node : ListTree → Tree

inductive ListTree : Type :=
  | nil : ListTree
  | cons : Tree → ListTree → ListTree
  deriving DecidableEq -- ... and we get an error here :-(
end
-- (Assume I want to use Finset late in the same file.)