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