Compute the context in the equation meta only once

[valis]

An expression of the form equation a b c d has 3 omitted proofs (namely, a = b, b = c, and c = d). The context will be computed for each of these proofs separately. We can optimize this by computing the context only once.

If some proof has a hint that modifies the context (e.g., equation a {using p} b c d or equation a {hiding p} b c), then we cannot use the common context in general. We probably still can reuse it if the hind only adds something to the context (as in the first example).