proposition: Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i := x]} ∪ m.
proof: Proof. apply map_eq. intros j. apply option_eq. intros y. rewrite lookup_union_Some_raw. destruct (decide (i = j)); subst. - rewrite !lookup_singleton, lookup_insert. intuition congruence. - rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence. Qed.
imports: Coq(Permutation) stdpp(options)