rw [sat_negate_iff_not_sat] at h2
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negateLiteral
⊢ False
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False