intro h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
⊢ p ⊨ delete c l → p ⊨ c
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
h : p ⊨ delete c l
⊢ p ⊨ c