{A : Type} {n : nat} (P : A -> Type) (x : A) : P x -> for_all P (repeat x n). Proof. intros H. induction n as [|n IHn]. 1: exact tt. exact (H, IHn). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum