I am trying to work through Andrew Pitts' chapter on categorical logic: Categorical Logic. On page 7 he presents a system of equational logic. The rules are listed below:
$$\dfrac{}{M = M : \sigma \ [\Gamma]}$$
$$\dfrac{M = M^{\prime} : \sigma \ [\Gamma]}{M^{\prime}= M : \sigma \ [\Gamma]}$$
$$\dfrac{M = M^{\prime} : \sigma \ [\Gamma] \quad M^{\prime} = M^{\prime \prime} : \sigma \ [\Gamma] }{M = M^{\prime \prime} : \sigma \ [\Gamma]} $$
$$\dfrac{M = M^{\prime} : \sigma \ [\Gamma] \quad N = N^{\prime} : \tau \ [\Gamma,x: \sigma, \Gamma^{\prime}]}{N[M/x] = N^{\prime}[M^{\prime}/x]: \tau \ [\Gamma,\Gamma^{\prime}]} $$
Where for instance $ M : \sigma \ [\Gamma] $ denotes that the term $M$ has sort $ \sigma $ and is given a context $ [\Gamma] $ which is a finite list of variable sort pairs which minimally include the variables occurring in the term $M$. Given the categorical semantics, it seems that if $ M = M^{\prime} : \sigma \ [\Gamma] $ is an equation in context, satisfied by a structure, then the structure should satisfy $ M = M^{\prime} : \sigma \ [\Gamma^{\prime \prime}] $ where $ [\Gamma^{\prime \prime}] $ is another context which contains $ [\Gamma] $ as a subsequence after possibly deleting some number of variable sort pairs. (I believe this because terms in context $M : \sigma \ [\Gamma]$ are interpreted as morphisms in a category with finite products and weakening of context corresponds to precomposition by a product of projection morphisms.)
However, on the syntactic side, I cannot seem to derive such a general form of weakening of the context of an equation. Given the rules for the system of equational logic I can only see how to derive the following less general context weakening rule: $$\dfrac{M = M^{\prime} : \sigma \ [\Gamma] }{M = M^{\prime} : \sigma \ [\Gamma,\Gamma^{\prime}]} $$ from $$\dfrac{}{x = x : \sigma \ [\Gamma, x:\sigma,\Gamma^{\prime}]} $$ and $$ \dfrac{M = M^{\prime} : \sigma \ [\Gamma] \quad x = x : \sigma \ [\Gamma,x: \sigma,\Gamma^{\prime}]}{M = M^{\prime} : \sigma \ [\Gamma,\Gamma^{\prime}]} $$
My question is: Is a more general context weakening rule derivable from the system or not? If not, should the system be extended to allow such a rule or is there a good reason not to have it?
Thank you very much for your consideration.