Agda: Derive equality *and* AVL dicts in the same program?

I'm doing some PL theory work in Agda, and I've run into this situation

• I need some kind of dictionary (like the Stdlib AVL trees) to encode finite maps.
• I need to derive equality for my types, since they have many constructors and a pairwise comparison is tedious.

Agda-prelude, provides the second but not the first, and the stdlib provides the first but not the second. The two are not compatible.

Are there existing libraries I can use that will give me both functionalities without conflicts? I'm not worried about performance, so if the finite maps are list-backed that's fine, but I'd prefer to not prove a bunch of theorems about them manually.