index_of@{i|} {A : Type@{i}} (l : list A) (x : A) : InList x l -> sig@{Set i} (fun n : nat => { H : (n < length l)%nat & nth' l n H = x }). Proof. induction l as [|a l IHl] using list_ind@{i i}. 1: intros x'; destruct x'. intros [| i]. - revert a p. snrapply paths_ind_r@{i i}. snrefine (exist@{i i} _ 0%nat _). snrefine (exist _ _ idpath). apply leq_succ. exact _. - destruct (IHl i) as [n [H H']]. snrefine (exist@{i i} _ n.+1%nat _). snrefine (_; _); cbn. 1: apply leq_succ, H. refine (_ @ H'). apply nth'_cons. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum