So, our proposal is, we can leave Var unspecified and no more exotic terms. Of course now, deriving meta-logical properties of a context is very difficult. And now a solution is to add axioms which describe essentially only what is strictly necessary for reasoning on context, and we have distilled these axioms form a very large case study precisely on proving meta-theoretical properties of the p-calculus.

---