rw [not]
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst =
    match l.snd with
    | true => false
    | false => true