inlist_map' {A B : Type} (f : A -> B) (l : list A) (x : B) : InList x (list_map f l) -> { y : A & (f y = x) * InList y l }. Proof. induction l as [|y l IHl]. 1: contradiction. intros [p | i]. - exact (y; (p, inl idpath)). - destruct (IHl i) as [y' [p i']]. exact (y'; (p, inr i')). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum