Theorem: LeanSAT.Model.PropFun.semVars_fls (LeanSAT/Model/PropVars.lean)

State before:
ν✝ : Sort ?u.573761
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
⊢ semVars ⊥ = ∅
Tactic:
ext
State after:
case a
ν✝ : Sort ?u.573761
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
a✝ : ν
⊢ a✝ ∈ semVars ⊥ ↔ a✝ ∈ ∅

State before:
case a
ν✝ : Sort ?u.573761
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
a✝ : ν
⊢ a✝ ∈ semVars ⊥ ↔ a✝ ∈ ∅
Tactic:
simp [mem_semVars]
State after:
no goals