simp [LitVar.satisfies_iff, PropAssignment.set] at hr h
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 ν
hd' : L
hd'_mem : hd' ∈ tl
h : PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar hd') = LitVar.polarity hd'
hr : ¬τ ⊨ LitVar.toPropFun hd'
⊢ ∃ 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 ν
hd' : L
hd'_mem : hd' ∈ tl
h : (if LitVar.toVar hd' = LitVar.toVar hd then !LitVar.polarity hd else τ (LitVar.toVar hd')) = LitVar.polarity hd'
hr : ¬τ (LitVar.toVar hd') = LitVar.polarity hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂