take_inlist@{i|} {A : Type@{i}} (n : nat) (l : list A) (x : A) : InList x (take n l) -> InList x l. Proof. intros H. induction l as [|a l IHl] in n, H, x |- * using list_ind@{i i}. 1: rewrite take_nil in H; contradiction. destruct n. 1: rewrite take_0 in H; contradiction. destruct H as [-> | H]. - left; reflexivity. - right; exact (IHl _ _ H). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum