proposition: Lemma map_subseteq_size_eq {A} (m1 m2 : M A) : m1 ⊆ m2 → size m2 ≤ size m1 → m1 = m2.
proof: Proof. intros. apply map_to_list_inj, submseteq_length_Permutation. - by apply map_to_list_submseteq. - by rewrite !map_to_list_length. Qed.
imports: Coq(Permutation) stdpp(options)