case h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.9278
B : Set M
s : Set (α → M)
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ setOf (Formula.Realize ⊥)
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.9278
B : Set M
s : Set (α → M)
⊢ ∅ = setOf (Formula.Realize ⊥)
ext
no goals
case h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.9278
B : Set M
s : Set (α → M)
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ setOf (Formula.Realize ⊥)
simp