intro s hs
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
⊢ ∀ (s : V), Inductive s → succ n ∈ s
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
s : V
hs : Inductive s
⊢ succ n ∈ s