proposition: Lemma map_empty_equiv_eq m : m ≡ ∅ ↔ m = ∅.
proof: Proof. split; [intros Hm; apply map_eq; intros i|intros ->]. - generalize (Hm i). by rewrite lookup_empty, None_equiv_eq. - intros ?. rewrite lookup_empty; constructor. Qed.
imports: Coq(Permutation) stdpp(options)