Definition nil_unique {X} (x : stn 0 -> X) : nil = (0,,x). Proof. intros. unfold nil. apply maponpaths. apply isapropifcontr. apply iscontr_vector_0. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.