proposition: Lemma map_compose_empty_l n : (∅ : MB C) ∘ₘ n =@{MA C} ∅.
proof: Proof. apply map_eq. intros k. rewrite map_lookup_compose, lookup_empty. destruct (n !! k); simpl; [|done]. apply lookup_empty. Qed.
imports: Coq(Permutation) stdpp(options)