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