simp_all [toPropFun, Array.mem_def]
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₂
case mp.mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
lits : List L
h : any ↑(List.map (fun x => LitVar.toPropFun x) lits) = ⊤
⊢ ∃ l₁ ∈ lits, ∃ l₂ ∈ lits, l₁ = -l₂