proposition: Lemma reverse_index {X : UU} (x : Sequence X) (i : stn (length x)) : (reverse x) (dualelement i) = x i.
proof: 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.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics