proposition: Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x : (∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
proof: Proof. intros ? j; destruct (decide (i = j)) as [->|]. - rewrite lookup_insert. destruct (m !! j); simpl; eauto. - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl. Qed.
imports: Coq(Permutation) stdpp(options)