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