{A : Type} (n : nat) (l : list A) (x : A) : InList x (remove n l) -> InList x l. Proof. unfold remove. intros p. apply equiv_inlist_app in p. revert p. snrapply sum_rec. - apply take_inlist. - apply drop_inlist. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum