. apply Or.inl
  simp [mkLit]
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))
no goals