proposition: Lemma isofhlevellist (n : nat) {X : UU} (is1 : isofhlevel (S (S n)) X) : isofhlevel (S (S n)) (list X).
proof: Proof. use isofhleveltotal2. - intros m k. apply isofhlevelsnprop, isasetnat. - intro m. apply isofhlevelvec, is1. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors