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