simp only [GoedelTranslation.atom_def, axiomFour!]
case hatom
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
a✝ : α
⊢ m𝓓 ⊢! Superintuitionistic.Formula.atom a✝ᵍ ⟶ □Superintuitionistic.Formula.atom a✝ᵍ
no goals