Definition vectorEquality {m : nat} (f : Vector X n) (g : Vector X m) (p : n = m) : (∏ i, f i = g (transportf stn p i)) -> transportf (Vector X) p f = g. Proof. intro. induction p. apply funextfun. assumption. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.