inlist_nth'@{i|} {A : Type@{i}} (l : list A) (n : nat) (H : (n < length l)%nat) : InList (nth' l n H) l. Proof. induction l as [|a l IHa] in n, H |- * using list_ind@{i i}. 1: destruct (not_lt_zero_r _ H). destruct n. 1: by left. right. apply IHa. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum