proposition: Lemma map_to_list_submseteq {A} (m1 m2 : M A) : m1 ⊆ m2 → map_to_list m1 ⊆+ map_to_list m2.
proof: Proof. intros; apply NoDup_submseteq; [by eauto using NoDup_map_to_list|]. intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken. Qed.
imports: Coq(Permutation) stdpp(options)