induction pr with
| hyp f h => exact hh _ (Or.inl h)
| var v => exact hh _ (Or.inr ⟨v, rfl⟩)
| @ax σ' a ha dj' hh' IH =>
  rw [← Formula.subst_tr]
  apply ax (subst.trans σ' σ) ha
  focus
    intros a b ab c d hc hd
    let ⟨e, ea, ce⟩ := Expr.mem_subst hc
    let ⟨f, fb, df⟩ := Expr.mem_subst hd
    refine dj _ _ ?_ _ _ ce df
    exact dj' _ _ ab _ _ ea fb
  focus { intros f; rw [Formula.subst_tr]; refine IH _ }
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
pr : Provable axs Γ' fmla
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
⊢ Provable axs Γ (Formula.subst σ fmla)
no goals