Definition tail (vecsn : Vector X (S n)) : Vector X n := vecsn ∘ dni (0,, natgthsn0 n).
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.