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.