proposition: Lemma map_empty {A} (m : M A) : m = ∅ ↔ ∀ i, m !! i = None.
proof: Proof. split. - intros -> i. by rewrite lookup_empty. - intros Hm. apply map_eq. intros i. by rewrite Hm, lookup_empty. Qed.
imports: Coq(Permutation) stdpp(options)