have := Provable.ax (Γ := ax.ctx) VR.expr H ?disj ?hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ Statement.provable' axs ax
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx (Formula.subst VR.expr ax.fmla)
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)