let ⟨f, fb, df⟩ := Expr.mem_subst hd
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))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
⊢ DJ.disj Γ.dj c d
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))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
f : VR
fb : f ∈' σ' b
df : d ∈' σ f
⊢ DJ.disj Γ.dj c d