case succ n h_ind =>
  cases h_ind
  case inl hex =>
    cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
  case inr hall =>
    if hpn : p n
    then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
    else
      apply Or.inr
      intro i hi
      cases hi
      case refl => exact hpn
      case step hstep => exact hall i hstep
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h_ind : (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
no goals