simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]
case conj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐒𝟒 ⊢! (p✝ ⋏ q✝ ⟶ p✝)ᵍ
case conj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⋏ q✝ᵍ ⟶ p✝ᵍ)