rw [← eta l]
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ l = mkPos (toVar l) ∨ l = mkNeg (toVar 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)))