simp only [subst_of]
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
⊢ Provable axs Γ (v.type, subst_of ((x, e) :: σ) v)
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
⊢ Provable axs Γ (v.type, if x = v then e else subst_of σ v)