proposition: Lemma vector_hlevel (X : UU) (n : nat) {m : nat} (ism : isofhlevel m X) : isofhlevel m (Vector X n).
proof: Proof. apply impred; auto. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics