refine if hr : any _ = ⊤ then have := ih hr; ?_ else ?_
case mp.mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
case mp.mk.cons.refine_1
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
this : ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
⊢ ∃ 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
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -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₂