exact ⟨Deduction.maxm $ hSubset hp⟩
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
p : Formula α
hp : p ∈ Ax(𝓓₁)
⊢ 𝓓₂ ⊢! p
no goals