rcases C with ⟨lits⟩
case mp
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
h : toPropFun C = ⊤
⊢ ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂
case mp.mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
lits : List L
h : toPropFun { data := lits } = ⊤
⊢ ∃ l₁ ∈ { data := lits }, ∃ l₂ ∈ { data := lits }, l₁ = -l₂