proposition: Lemma map_disjoint_compose_l m1 m2 n : m1 ##ₘ m2 → m1 ∘ₘ n ##ₘ m2 ∘ₘ n.
proof: Proof. rewrite !map_disjoint_spec; intros Hdisj a c1 c2. rewrite !map_lookup_compose. destruct (n !! a); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)