Dependent tree map lemmas #
This file contains lemmas about Std.Data.DTreeMap.Raw.Basic. Most of the lemmas require
TransCmp cmp for the comparison function cmp and a proof that the involved maps are well-formed.
These proofs can be obtained from Std.Data.DTreeMap.Raw.WF.
This is a restatement of mem_of_mem_insertIfNew that is written to exactly match the
proof obligation in the statement of get_insertIfNew.
Deprecated, use forMUncurried_eq_forM_toList together with forM_eq_forMUncurried instead.
Deprecated, use forInUncurried_eq_forIn_toList together with forIn_eq_forInUncurried instead.
A variant of contains_of_contains_insertMany_list used in get_insertMany_list.
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.