simp_all only [Bool.false_eq_true]
case hLoeb
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasLoeb✝ : 𝐊𝟒(𝐇).rules.loeb = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐇) ⊢! □p✝ ⟶ p✝
a✝ : 𝐊𝟒𝐇 ⊢! □p✝ ⟶ p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
no goals