simp only [mem_sep_iff, interpret_isNat', interpret_inr, and_iff_right_iff_imp]
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ sep (BoundedFormula.isNat (Sum.inr 0)) (fun i => Empty.elim i) Infinity.inductiveSet ↔
    ∀ (s : V), Inductive s → n ∈ s
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ (∀ (y : V), Inductive y → n ∈ y) → n ∈ Infinity.inductiveSet