Lemma reverse_index' {X : UU} (x : Sequence X) (i : stn (length x)) : (reverse x) i = x (dualelement i). Proof. cbn. unfold dualelement, coprod_rect. induction (natchoice0 (length x)) as [H' | H']. - apply maponpaths. apply isinjstntonat. cbn. apply idpath. - apply maponpaths. apply isinjstntonat. cbn. apply idpath. Qed.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.