induction n
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
⊢ (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
case zero
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i

case succ
p : Nat → Prop
inst✝ : DecidablePred p
n✝ : Nat
n_ih✝ : (∃ i, i < n✝ ∧ p i) ∨ ∀ (i : Nat), i < n✝ → ¬p i
⊢ (∃ i, i < succ n✝ ∧ p i) ∨ ∀ (i : Nat), i < succ n✝ → ¬p i