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