cases polarity l
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) (polarity l) = mkPos (toVar (mkLit L (toVar l) (polarity l))) ∨
    mkLit L (toVar l) (polarity l) = mkNeg (toVar (mkLit L (toVar l) (polarity l)))
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))

case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))