The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hello,

In the Reference Manual (Section 4.2 : Typed Terms)
there is this rule:


      𝓦𝓕(E)[Γ]    (x:T) ∈ Γ or (x:=t:T) ∈ Γ for some t
  Var ─────────────────────────────────────────────────
                         E[Γ] ⊢ x:T


Isn't that rule, as it is stated, too weak?
Shouldn't the rule read:

      𝓦𝓕(E)[Γ]    (x:T) ∈ E∪Γ or (x:=t:T) ∈ E∪Γ for some t
  Var ─────────────────────────────────────────────────────
                         E[Γ] ⊢ x:T

?

Otherwise, how would one be able to prove that x:T
if  (x,T) ∈ E
but (x,T) ∉ Γ
?