exact hh _ (Or.inr ⟨v, rfl⟩)
case var
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)
v : VR
⊢ Provable axs Γ (Formula.subst σ (VR.vhyp v))
no goals