rw [← inst.out]
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
⊢ Provable axs Γ (c, e)
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
⊢ Provable axs Γ (c, Expr.subst σ s)