dsimp [toPropForm, toPropFun]
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦toPropForm l⟧ = toPropFun l
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))⟧ =
    if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ