constructor
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ toPropFun C = ⊤ ↔ ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂
case mp
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ toPropFun C = ⊤ → ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂

case mpr
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ (∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂) → toPropFun C = ⊤