Definition sequenceEquality2 {X} (f g:Sequence X) (p:length f=length g) : (∏ i, f i = g (transportf stn p i)) -> f = g. Proof. intros e. induction f as [m f]. induction g as [n g]. simpl in p. apply (total2_paths2_f p). now apply vectorEquality. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.