(n : nat) (P : nat -> Type) (H1 : forall k, P k -> (k < n)%nat) (H2 : forall k, Decidable (P k)) : Decidable (exists k, P k). Proof. nrapply decidable_iff. 1: apply iff_inverse; nrapply list_exists_seq. 1: exact H1. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum