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