cases polarity l <;> simp [PropForm.vars]
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropForm.vars (if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))) =
    {toVar l}
no goals