proposition: Lemma map_compose_union_l m1 m2 n : (m1 ∪ m2) ∘ₘ n = (m1 ∘ₘ n) ∪ (m2 ∘ₘ n).
proof: Proof. apply map_eq; intros a. rewrite lookup_union, !map_lookup_compose. destruct (n !! a) as [b|] eqn:?; simpl; [|done]. by rewrite lookup_union. Qed.
imports: Coq(Permutation) stdpp(options)