proposition: Lemma map_subseteq_inv {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ⊂ m2 ∨ m1 = m2.
proof: Proof. intros. destruct (decide (m2 ∖ m1 = ∅)) as [Hm21|(i&x&Hi)%map_choose]. - right. by rewrite <-(map_difference_union m1 m2), Hm21, (right_id_L _ _). - left. apply lookup_difference_Some in Hi as [??]. apply map_subset_alt; eauto. Qed.
imports: Coq(Permutation) stdpp(options)