{n : nat} (P : nat -> Type) (H : forall k, P k -> (k < n)%nat) : (exists k, P k) <-> list_exists P (seq n). Proof. split. - intros [k p]. snrapply (list_exists_inlist P _ k _ p). apply inlist_seq, H. exact p. - intros H1. apply inlist_list_exists in H1. destruct H1 as [k [Hk p]]. exists k. exact p. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum