proposition: Lemma map_filter_singleton i x : filter P {[i := x]} =@{M A} if decide (P (i, x)) then {[i := x]} else ∅.
proof: Proof. by rewrite <-!insert_empty, map_filter_insert, delete_empty, map_filter_empty. Qed.
imports: Coq(Permutation) stdpp(options)