proposition: Lemma map_compose_img_subseteq `{SemiSet C D} m n : map_img (m ∘ₘ n) ⊆@{D} map_img m.
proof: Proof. intros c. rewrite !elem_of_map_img. setoid_rewrite map_lookup_compose_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)