Skip to content

Non-canonical FinMap?

Is there any interest in generalizing FinMap to use a setoid equality? I have a non-canonical finite map that I need to use, but I can't leverage lemmas built from the FinMap class.