induction' n with n IH
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin n → Semiformula L ξ 1
q : Semiformula L ξ n
⊢ (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
case zero
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin 0 → Semiformula L ξ 1
q : Semiformula L ξ 0
⊢ (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin 0 → M), (∀ (i : Fin 0), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q

case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (Evalf s ε) (ballClosure p q) ↔
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q