proposition: Lemma lookup_difference {A} (m1 m2 : M A) i : (m1 ∖ m2) !! i = match m2 !! i with None => m1 !! i | _ => None end.
proof: Proof. unfold difference, map_difference; rewrite lookup_difference_with. destruct (m1 !! i), (m2 !! i); done. Qed.
imports: Coq(Permutation) stdpp(options)