simp [hEq, this]
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬p = polarity l
hEq : x = toVar l
this : (!p) = polarity l
⊢ l = mkLit L x !p
no goals