intro i hi
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ∀ (i : Nat), i < succ n → ¬p i
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hi : i < succ n
⊢ ¬p i