constructor
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd