apply conj₂!
case hConj₂
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! p✝ ⋏ q✝ ⟶ q✝
no goals