proposition: Lemma map_filter_union_complement {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) : filter P m ∪ filter (λ v, ¬ P v) m = m.
proof: Proof. apply map_eq; intros i. apply option_eq; intros x. rewrite lookup_union_Some, !map_lookup_filter_Some by auto using map_disjoint_filter_complement. destruct (decide (P (i,x))); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)