exact hh _ (Or.inl h)
case hyp
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)
f : Formula
h : f ∈ Γ'.hyps
⊢ Provable axs Γ (Formula.subst σ f)
no goals