Lemma reversereverse {X : UU} (x : Sequence X) : reverse (reverse x) = x. Proof. induction x as [n x]. apply pair_path_in2. apply funextfun; intro i. unfold reverse, dualelement, coprod_rect. cbn. induction (natchoice0 n) as [H | H]. + apply fromempty. rewrite <- H in i. now apply negstn0. + cbn. apply maponpaths. apply isinjstntonat. apply minusminusmmn. apply natgthtogehm1. apply stnlt. Qed.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.