proposition: Lemma map_compose {A B C : UU} (f : A → B) (g : B → C) (xs : list A) : map (g ∘ f) xs = map g (map f xs).
proof: Proof. revert xs. apply list_ind. - apply idpath. - intros x xs IH. now rewrite !map_cons, IH. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors