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