Definition vecS_eq {n} {u v : vec A (S n)} (p : hd u = hd v) (q : tl u = tl v) : u = v := dirprod_paths p q.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.