simp_all only [Bool.false_eq_true]
case hHenkin
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasHenkin✝ : 𝐆𝐋.rules.henkin = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! □p✝ ⟷ p✝
a✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟷ p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
no goals