proposition: Lemma map_filter_id m : (∀ i x, m !! i = Some x → P (i, x)) → filter P m = m.
proof: Proof. intros Hi. apply map_eq. intros i. rewrite map_lookup_filter. destruct (m !! i) eqn:Hlook; [|done]. apply option_guard_True, Hi, Hlook. Qed.
imports: Coq(Permutation) stdpp(options)