Extensional maps

[Kaptch]

Description

Beyond what quotient PR did, this PR is mostly the extensional maps preps before moving to equality for OFEs:

• Made partial maps extensional by default. Folded the old ExtensionalPartialMap class into LawfulPartialMap (it now carries equiv_iff_eq), so pointwise-equivalent maps are just equal. As a result ~40 map lemmas (insert_delete, union_*, map_*, zip_*, etc) now conclude = instead of ≡ₘ, and a lot of downstream proofs collapse to rw/subst.
• Dropped the ≡ₘ case from map induction. Induction_on no longer needs the hequiv obligation, which deleted that case everywhere maps are inducted (BigOp, BigSepMap, Plainly, GenHeap, HeapView).
• Removed now dead map implementations. The whole AssocList type (can restore with PartialMap instance) and the plain TreeMap instances are gone, the only instances of LawfulPartialMap are functions and ExtTreeMap.

Added Leibniz instances for dependent functions, GenMap, ReservationMap, and HeapView. With that, all constructions in the project should be Leibniz/Leibniz-preserving.

There is some simplification (~230 lines), but the ≡ that is introduced on BI level cuts short the gain from it.

Builds on top of #485

[MackieLoeffel]

Is it still necessary to have PartialMap.equiv or can it just be replaced by equality?

[Kaptch]

Do you mean changing the rules to be stated without get? I think it can be done as well, I did it this way to reuse most of the file + allow users to use extensionality while staying in the interface, in case they define some additional operations on top of maps. I can change it, if you think that it's better to avoid PartialMap.equiv completely.

[Kaptch]

Rebased it on top of the agreement PR, so now all OFEs implemented in the project are Leibniz. I tried to stay as close as possible to the old interfaces, but if you think that we should use equalities instead of equiv, I can make a pass and change it now.
I would postpone interface changes to the point after the OFE change to have a complete setup that allows to drop setoids (mostly, to make sure that porting can be done mechanically).

As a side note, we probably should discuss at some point having version tags and a changelog for interface changes.