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