Theorem: varSubPreservesType (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
x : V
σ : 𝕋 𝕍
⊢ ∀ {Γ : TCtxt V 𝕍}, (Γ ⊢ N : σ) → typeOf (Γ;; x : σ) M = typeOf Γ (subVarInTerm x N M)
Tactic:
sorry
State after:
no goals