Lemma map_idfun {A : UU} (xs : list A) : map (idfun A) xs = 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.