Context weakening as an explicit rule for languages of the the lambda cube?
If you intend to formalize meta-theorems in a proof assistant, then it's probably better to avoid the general weakening rule because it will pollute all your inductive arguments. Every single induction on the derivation will contain the case &quot;but what if the context got larger using weakening?&quot; and that's going to be super annoying. I would recommend instead a sane variable rule and no weakening. You can always show that weaking is admissible.
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}$$