proposition: Lemma map_compose_empty_iff m n : m ∘ₘ n = ∅ ↔ ∀ a b, n !! a = Some b → m !! b = None.
proof: Proof. rewrite map_empty. setoid_rewrite map_lookup_compose_None. apply forall_proper; intros a. destruct (n !! a); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)