nth_list_map@{i j|} {A : Type@{i}} {B : Type@{j}} (f : A -> B) (l : list A) (n : nat) : nth (list_map f l) n = functor_option f (nth l n). Proof. induction l as [|a l IHl] in n |- * using list_ind@{i j}. 1: by destruct n. 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