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
hall : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
no goals