rcases hr with ⟨τ,hr⟩
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
hr : ∃ x, ∀ x_1 ∈ tl, ¬x ⊨ LitVar.toPropFun x_1
h : ∀ (τ : PropAssignment ν), τ ⊨ LitVar.toPropFun hd ∨ ∃ a ∈ tl, τ ⊨ LitVar.toPropFun a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : ∀ (τ : PropAssignment ν), τ ⊨ LitVar.toPropFun hd ∨ ∃ a ∈ tl, τ ⊨ LitVar.toPropFun a
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂