rcases h with ⟨hd',hd'_mem,h⟩
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
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
h : ∃ a ∈ tl, PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar a) = LitVar.polarity a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
hd' : L
hd'_mem : hd' ∈ tl
h : PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar hd') = LitVar.polarity hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂