nth'_nth' {A} (l : list A) (n : nat) (H H' : (n < length l)%nat) : nth' l n H = nth' l n H'. Proof. apply ap, path_ishprop. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum