inlist_repeat@{i|} {A : Type@{i}} (n : nat) (x y : A) : InList y (repeat x n) -> y = x. Proof. induction n as [|n IHn]. 1:contradiction. intros [p | i]. - by symmetry. - by 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