length_seq_rev@{} (n : nat) : length (seq_rev n) = n. Proof. induction n as [|n IHn]. 1: reflexivity. cbn; f_ap. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum