Definition vector_stn_proofirrelevance {vec : Vector X n} {i j : stn n} : (stntonat _ i = stntonat _ j) -> vec i = vec j. Proof. intro. apply maponpaths, isinjstntonat; assumption. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.