Skip to content

Misc lemmas for maps

Robbert Krebbersrequested to merge
robbert/misc_map into master
  • Add lemmas merge_empty_l and merge_empty_r.
  • Add lemma map_filter_lookup.
  • Add lemma map_fmap_singleton_inv.

Merge request reports