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.