apply LawfulLitVar.ext <;> aesop
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h :
  (if polarity l1 = true then var (toVar l1) else (var (toVar l1))ᶜ) =
    if polarity l2 = true then var (toVar l2) else (var (toVar l2))ᶜ
⊢ l1 = l2
no goals