exact ax σ (haxs _ ha) (h₁.mono (DJ.refl _) hΓ.2) fun e h => IH _ h
case ax
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
σ : VR → Expr
ax✝ : Statement
ha : axs₁ ax✝
h₁ : DJ.subst σ ax✝.ctx.dj Γ₁.dj
a✝ : ∀ (h : Formula), (h ∈ ax✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs₁ Γ₁ (Formula.subst σ h)
IH : ∀ (h : Formula), (h ∈ ax✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs₂ Γ₂ (Formula.subst σ h)
⊢ Provable axs₂ Γ₂ (Formula.subst σ ax✝.fmla)
no goals