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