proposition: Lemma map_compose_min_r_dom {C} `{FinMap K' M', !RelDecision (∈@{D})} (m : M C) (n : M' K) : m ∘ₘ n = m ∘ₘ filter (λ '(_,b), b ∈ dom m) n.
proof: Proof. rewrite map_compose_min_r. f_equal. apply map_filter_ext. intros. by rewrite elem_of_dom. Qed.
imports: stdpp(options)