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. revert xs. apply list_ind. - apply idpath. - intros x xs IH. now rewrite !map_cons, IH. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.