intros f
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) h)
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
f : Formula
⊢ (f ∈ a.ctx.hyps ∨ ∃ v, f = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) f)