# Context weakening as an explicit rule for languages of the the lambda cube?

I'm trying to formalize the syntax and typing judgments of the Calculus of Constructions in Coq. I'm choosing to use the Pure Type Systems presentation of CoC; however, I've seen mild variations in the rules for PTS in different resources.

In Type Theory and Formal Proof: An Introduction, Nederpelt and Geuvers add context weakening as an explicit rule:

Γ ⊢ e : T
x \notin Γ
Γ ⊢ U : s
---------------------- t_weak
Γ, x : U ⊢ e : T

---------------------- t_var
Γ, x : T ⊢ x : T


Their formalization clearly requires t_weak, since t_var can only type the last variable in the context.

In ATAPL, Pierce instead chooses a more powerful rule for typing variables, and forgoes an explicit context weakening rule.

x : T \in Γ
----------- t_var'
Γ ⊢ x : T


Presumably, one would be able to derive a weakening rule from the rules Pierce chooses.

Are both these systems indeed equivalent? Is there any reason to choose one over the other for the sake of formalization in a proof assistant?

As far as sane variable rules go, the one you quoted works well when variables are symbols and contexts are maps taking symbols to their types. If you indent to use de Bruijn indices, then you should use different variable rules (note that contexts are just lists of types because variable names are just natural numbers): $$\frac{ }{\Gamma, A \vdash \mathtt{var}_0 : A} \qquad \frac{\Gamma \vdash \mathtt{var}_k : B}{\Gamma, A \vdash \mathtt{var}_{\mathtt{succ}(k)} : B}$$