dsimp [mkLit]
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ toVar (mkLit L x p) = x
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ toVar (if p = true then mkPos x else mkNeg x) = x