{A B : Type} (f : A -> B) (l : list A) (x : A) : InList x l -> InList (f x) (list_map f l). Proof. simple_list_induction l y l IHl. 1: contradiction. intros [p | i]. - left. exact (ap f p). - right. exact (IHl i). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum