case inl hex =>
  cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hex : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
no goals