rw [PropFun.ext_iff] at hr h
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : ¬any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : ∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) ↔ τ ⊨ ⊤
hr : ¬∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) tl) ↔ τ ⊨ ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂