Definition seq_key_eq_lemma' {X :UU} (g g' : Sequence X) : length g = length g' -> (∏ i, ∑ ltg : i < length g, ∑ ltg' : i < length g', g (i ,, ltg) = g' (i ,, ltg')) -> g=g'. Proof. intros k r. apply seq_key_eq_lemma. * assumption. * intros. induction (r i) as [ p [ q e ]]. simple refine (_ @ e @ _). - now apply maponpaths, isinjstntonat. - now apply maponpaths, isinjstntonat. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.