List/Theory: add decidable_exists_bounded_nat

HoTT · Jan 15, 2025 · e235678 · e235678
1 parent 6f18b61
commit e235678
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/theories/Spaces/List/Theory.v b/theories/Spaces/List/Theory.v
@@ -1249,3 +1249,8 @@ Proof.
   1: exact H1.
   exact _.
 Defined.
+
+Definition decidable_exists_bounded_nat (n : nat) (P : nat -> Type)
+  (H2 : forall k, Decidable (P k))
+  : Decidable { k : nat & prod (k < n) (P k) }
+  := decidable_exists_nat n _ (fun k => fst) _.