proposition: Lemma fmap_empty_iff {A B} (f : A → B) m : f <$> m =@{M B} ∅ ↔ m = ∅.
proof: Proof. split; [|intros ->; by rewrite fmap_empty]. intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm). by rewrite lookup_fmap, !lookup_empty, fmap_None. Qed.
imports: Coq(Permutation) stdpp(options)