proposition: Lemma map_compose_min_r m n : m ∘ₘ n = m ∘ₘ filter (λ '(_,b), is_Some (m !! b)) n.
proof: Proof. apply map_eq; intros a. rewrite !map_lookup_compose, map_lookup_filter. destruct (n !! a) as [b|] eqn:?; simpl; [|done]. by destruct (m !! b) eqn:?. Qed.
imports: Coq(Permutation) stdpp(options)