proposition: Lemma weq_vector_1 {X : UU} : X ≃ Vector X 1.
proof: Proof. intermediate_weq (unit → X). - apply invweq, weqfunfromunit. - apply weqbfun. exact weqstn1tounit. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics