proposition: Lemma map_img_empty_iff m : map_img m ≡ ∅ ↔ m = ∅.
proof: Proof. split; [|intros ->; by rewrite map_img_empty]. intros Hm. apply map_empty; intros i. apply eq_None_ne_Some; intros x ?%elem_of_map_img_2. set_solver. Qed.
imports: Coq(Permutation) stdpp(options)