Naming of roundtrip lemmas is confusing
The naming convention of roundtrip lemmas is confusing as the name is opposite to the operation described by the lemma. E.g. consider:
map_to_list_to_map : ∀ l : list (A * B), NoDup l.(tgt) → map_to_list (list_to_map l) ≡ₚ l
Note that map_to_list_to_map
not about the conversion "map to list to map", but about the conversion "list to map to list".
@jung suggested the naming map_to_list_list_to_map
.
See discussion at !254 (comment 66702)