Theorem: var_rule (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x : V
σ : 𝕋 𝕍
⊢ getType x Γ = some σ ↔ (Γ ⊢ Λ.Var x : σ)
Tactic:
simp
State after:
no goals