theories/fin_maps.v · 9cbafb674abd6efb154559eb603b9599ae94c5ec · Arthur Azevedo de Amorim / stdpp

Forked from Iris / stdpp

Source project has a limited visibility.

6 years ago

Inline equality premise in `map_insert_zip_with`. · 9cbafb67

Two reasons:

- The equality makes it very hard to use the lemma with `rewrite`.
- The version for lists `insert_zip_with` does not have the equality either.

9cbafb67

History

Inline equality premise in `map_insert_zip_with`.

Robbert Krebbers authored 6 years ago

Two reasons:

- The equality makes it very hard to use the lemma with `rewrite`.
- The version for lists `insert_zip_with` does not have the equality either.