Definition seq_key_eq_lemma {X :UU}( g g' : Sequence X)(e_len : length g = length g') (e_el : forall ( i : nat )(ltg : i < length g )(ltg' : i < length g' ), g (i ,, ltg) = g' (i ,, ltg')) : g=g'. Proof. intros. induction g as [m g]; induction g' as [m' g']. simpl in e_len, e_el. intermediate_path (m' ,, transportf (λ i, stn i -> X) e_len g). - apply transportf_eq. - apply maponpaths. intermediate_path (g ∘ transportb stn e_len). + apply transportf_fun. + apply funextfun. intro x. induction x as [ i b ]. simple refine (_ @ e_el _ _ _). * simpl. apply maponpaths. apply transport_stn. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.