rw [Formula.subst_id]
axs : Statement → Prop
ax : Statement
H : axs ax
fmla✝ : Formula
h✝ : fmla✝ ∈ ax.ctx.hyps ∨ ∃ v, fmla✝ = VR.vhyp v
fmla : Formula
h : fmla ∈ ax.ctx.hyps
⊢ Provable axs ax.ctx (Formula.subst VR.expr fmla)
axs : Statement → Prop
ax : Statement
H : axs ax
fmla✝ : Formula
h✝ : fmla✝ ∈ ax.ctx.hyps ∨ ∃ v, fmla✝ = VR.vhyp v
fmla : Formula
h : fmla ∈ ax.ctx.hyps
⊢ Provable axs ax.ctx fmla