proposition: Lemma map_difference_filter {A} (m1 m2 : M A) : m1 ∖ m2 = filter (λ kx, m2 !! kx.1 = None) m1.
proof: Proof. apply map_eq; intros i. apply option_eq; intros x. by rewrite lookup_difference_Some, map_lookup_filter_Some. Qed.
imports: Coq(Permutation) stdpp(options)