apply bfind_prop (λ n => decide (p n))
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ decide (p (find p h)) = true
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ ∃ n, decide (p n) = true