induction pr with
| hyp e h => exact hyp e (hΓ.1 _ h)
| var v => exact var v
| ax σ ha h₁ _ IH =>
  exact ax σ (haxs _ ha) (h₁.mono (DJ.refl _) hΓ.2) fun e h => IH _ h
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
pr : Provable axs₁ Γ₁ e
⊢ Provable axs₂ Γ₂ e
no goals