proposition: Lemma map_cons {A B : UU} (f : A -> B) (x : A) (xs : list A) : map f (cons x xs) = cons (f x) (map f xs).
proof: Proof. apply idpath. Qed.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors