proposition: Lemma map_compose_assoc `{FinMap A MA, FinMap B MB, FinMap C MC} {D} (m : MC D) (n : MB C) (o : MA B) : m ∘ₘ (n ∘ₘ o) = (m ∘ₘ n) ∘ₘ o.
proof: Proof. apply map_eq; intros a. rewrite !map_lookup_compose. destruct (o !! a); simpl; [|done]. by rewrite map_lookup_compose. Qed.
imports: Coq(Permutation) stdpp(options)