nth'_repeat@{i|} {A : Type@{i}} (x : A) (i n : nat) (H : (i < length (repeat x n))%nat) : nth' (repeat x n) i H = x. Proof. induction n as [|n IHn] in i, H |- * using nat_ind@{i}. 1: destruct (not_lt_zero_r _ H). destruct i. 1: reflexivity. apply IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum