proposition: Lemma insert_subseteq_r {A} (m1 m2 : M A) i x : m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]>m2.
proof: Proof. intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono. Qed.
imports: Coq(Permutation) stdpp(options)