exact HenkinRule.henkin! ihp
case hHenkin
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasHenkin✝ : 𝐊𝟒(𝐇).rules.henkin = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐇) ⊢! □p✝ ⟷ p✝
ihp : 𝐊𝟒𝐇 ⊢! □p✝ ⟷ p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
no goals