simp at h1
v u : VarName
T : Finset VarName
x y : VarName
S : Finset VarName
h1 : v = x ∨ v = y → u ∉ S ∪ T
⊢ v = x ∨ v = y → u ∉ S
v u : VarName
T : Finset VarName
x y : VarName
S : Finset VarName
h1 : v = x ∨ v = y → u ∉ S ∧ u ∉ T
⊢ v = x ∨ v = y → u ∉ S