{A : Type} (l l' : list A) (x : A) : InList x l + InList x l' <~> InList x (l ++ l'). Proof. induction l as [|a l IHl]. - apply sum_empty_l. - cbn; nrefine (_ oE equiv_sum_assoc _ _ _). by apply equiv_functor_sum_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum