exact LoebRule.loeb! ihp
case hLoeb
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasLoeb✝ : 𝐊𝟒(𝐋).rules.loeb = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟶ p✝
ihp : 𝐊𝟒(𝐇) ⊢! □p✝ ⟶ p✝
⊢ 𝐊𝟒(𝐇) ⊢! p✝
no goals