length_repeat@{i|} {A : Type@{i}} (n : nat) (x : A) : length (repeat x n) = n. Proof. induction n using nat_ind@{i}. - reflexivity. - exact (ap S IHn). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum