proposition: Lemma map_not_Forall (m : M A) : ¬map_Forall P m ↔ ∃ i x, m !! i = Some x ∧ ¬P i x.
proof: Proof. split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto]. rewrite map_Forall_to_list. intros Hm. apply (not_Forall_Exists _), Exists_exists in Hm. destruct Hm as ([i x]&?&?). exists i, x. by rewrite <-elem_of_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)