proposition: Lemma merge_singleton i x y z : f (Some y) (Some z) = Some x → merge f {[i := y]} {[i := z]} =@{M C} {[i := x]}.
proof: Proof. intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto. Qed.
imports: Coq(Permutation) stdpp(options)