proposition: Lemma map_intersection_filter {A} (m1 m2 : M A) : m1 ∩ m2 = filter (λ kx, is_Some (m1 !! kx.1) ∧ is_Some (m2 !! kx.1)) (m1 ∪ m2).
proof: Proof. apply map_eq; intros i. apply option_eq; intros x. rewrite lookup_intersection_Some, map_lookup_filter_Some, lookup_union; simpl. unfold is_Some. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)