Extensional dependent hash map lemmas #
This file contains lemmas about Std.ExtDHashMap
.
This is a restatement of contains_of_contains_insertIfNew
that is written to exactly match the proof
obligation in the statement of get_insertIfNew
.
This is a restatement of mem_of_mem_insertIfNew
that is written to exactly match the proof obligation
in the statement of get_insertIfNew
.
Simpler variant of get?_filterMap
when LawfulBEq
is available.
Simpler variant of get_filterMap
when LawfulBEq
is available.
Simpler variant of get!_filterMap
when LawfulBEq
is available.
Simpler variant of getD_filterMap
when LawfulBEq
is available.
Simpler variant of get?_filter
when LawfulBEq
is available.
Simpler variant of get!_filter
when LawfulBEq
is available.
Simpler variant of getD_filter
when LawfulBEq
is available.
Variant of get?_map
that holds with EquivBEq
(i.e. without LawfulBEq
).
Variant of get_map
that holds with EquivBEq
(i.e. without LawfulBEq
).
Variant of get!_map
that holds with EquivBEq
(i.e. without LawfulBEq
).
Variant of getD_map
that holds with EquivBEq
(i.e. without LawfulBEq
).