proposition: Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom m1 ⊂ dom m2.
proof: Proof. intros [Hss1 Hss2]; split; [by apply subseteq_dom |]. contradict Hss2. rewrite map_subseteq_spec. intros i x Hi. specialize (Hss2 i). rewrite !elem_of_dom in Hss2. destruct Hss2; eauto. by simplify_map_eq. Qed.
imports: stdpp(options)