cases h
case inl
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
h : x = v
⊢ Provable axs Γ (v.type, e)
case inl.refl
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
⊢ Provable axs Γ (x.type, e)