rw [sat_iff, h, not] at pl
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl :
  (match l.snd with
    | true => false
    | false => true) =
    l.snd
⊢ False