proposition: Lemma isofhlevelvec {n} (is1 : isofhlevel n A) k : isofhlevel n (vec A k).
proof: Proof. induction k as [|k IH]. - apply isofhlevelcontr, iscontrunit. - apply isofhleveldirprod. + apply is1. + apply IH. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers