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

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

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