intro p
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
⊢ limplies α (insert f c) f
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ p ⊨ insert f c → p ⊨ f