case hyp =>
  intro fmla h
  match fmla, h with
  | fmla, Or.inl h => rw [Formula.subst_id]; exact Provable.hyp _ h
  | _, Or.inr ⟨v, rfl⟩ => exact Provable.var v
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
no goals