nth'_list_map@{i j|} {A : Type@{i}} {B : Type@{j}} (f : A -> B) (l : list A) (n : nat) (H : (n < length l)%nat) (H' : (n < length (list_map f l))%nat) : nth' (list_map f l) n H' = f (nth' l n H). Proof. induction l as [|a l IHl] in n, H, H' |- * using list_ind@{i j}. 1: destruct (not_lt_zero_r _ H). destruct n. 1: reflexivity. apply IHl. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum