Inconsistent naming of dom lemmas
The vast majority of dom
lemmas does not contain map
in their name since only maps have domains. There are some exceptions though:
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom m1 ## dom m2.
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom m1 ## dom m2.
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom m1 ## dom m2 → m1 ##ₘ m2.
Those should probably be renamed to remove the leading map_
. And maybe move the dom_
to the front?
Edited by Ralf Jung