proposition: Lemma insert_subseteq_l {A} (m1 m2 : M A) i x : m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
proof: Proof. intros Hi Hincl. etrans; [apply insert_mono, Hincl|]. by rewrite insert_id. Qed.
imports: Coq(Permutation) stdpp(options)