fact: Definition const_vec {X : UU} {n : nat} (x : X) : Vector X n := λ _, x.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics