Theorem: LeanSAT.polarity_eq (LeanSAT/Data/ICnf.lean)

State before:
l₁ l₂ : ILit
⊢ polarity l₁ = polarity l₂ ↔ (0 < ↑l₁ ↔ 0 < ↑l₂)
Tactic:
simp [polarity]
State after:
no goals