obtain ⟨_, e⟩ := hL
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝