unfold BoundedFormula.isInductive
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isInductive x) v l ↔ Inductive (interpretTerm V v l x)
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    Inductive (interpretTerm V v l x)