Lemma map_homot {A B : UU} {f g : A → B} (h : f ~ g) (xs : list A) : map f xs = map g xs. Proof. revert xs. apply list_ind. - apply idpath. - intros x xs IH. now rewrite !map_cons, h, IH. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.