Commit f6b0626b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Misc map_to_list properties.

parent 4e11257b
......@@ -671,6 +671,12 @@ Proof.
rewrite elem_of_map_to_list in Hlookup. congruence.
- by rewrite !map_of_to_list.
Lemma map_to_list_contains {A} (m1 m2 : M A) :
m1 m2 map_to_list m1 `contains` map_to_list m2.
intros; apply NoDup_contains; auto using NoDup_map_to_list.
intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = .
Proof. done. Qed.
Lemma map_of_list_cons {A} (l : list (K * A)) i x :
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment