Extensional dependent tree map lemmas #
This file contains lemmas about Std.ExtDTreeMap
.
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 LawfulEqCmp
is available.
Simpler variant of get_filterMap
when LawfulEqCmp
is available.
Simpler variant of get!_filterMap
when LawfulEqCmp
is available.
Simpler variant of getD_filterMap
when LawfulEqCmp
is available.
Simpler variant of get?_filter
when LawfulEqCmp
is available.
Simpler variant of get!_filter
when LawfulEqCmp
is available.
Simpler variant of getD_filter
when LawfulEqCmp
is available.
Variant of get?_map
that holds without LawfulEqCmp
.
Variant of get_map
that holds without LawfulEqCmp
.
Variant of get!_map
that holds without LawfulEqCmp
.
Variant of getD_map
that holds without LawfulEqCmp
.