obtain ⟨_, _, e⟩ := hH
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.H w✝