proposition: Lemma map_compose_min_l `{SemiSet B D, !RelDecision (∈@{D})} m n : m ∘ₘ n = filter (λ '(b,_), b ∈ map_img (SA:=D) n) m ∘ₘ n.
proof: Proof. apply map_eq; intros a. rewrite !map_lookup_compose. destruct (n !! a) as [b|] eqn:?; simpl; [|done]. rewrite map_lookup_filter. destruct (m !! b) eqn:?; simpl; [|done]. by rewrite option_guard_True by (by eapply elem_of_map_img_2). Qed.
imports: Coq(Permutation) stdpp(options)