proposition: Lemma lookup_difference_with {A} (f : A → A → option A) (m1 m2 : M A) i : difference_with f m1 m2 !! i = difference_with f (m1 !! i) (m2 !! i).
proof: Proof. unfold difference_with, map_difference_with. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)