  Many well-known logical identities are naturally written as equivalences
between contextual formulas. A simple example is the Boole-Shannon expansion
$c[p] \equiv (p \wedge c[\mathrm{true}] ) \vee (\neg\, p \wedge
c[\mathrm{false}] )$, where $c$ denotes an arbitrary formula with possibly
multiple occurrences of a "hole", called a context, and $c[\varphi]$ denotes
the result of "filling" all holes of $c$ with the formula $\varphi$. Another
example is the unfolding rule $\mu X. c[X] \equiv c[\mu X. c[X]]$ of the modal
$\mu$-calculus.
  We consider the modal $\mu$-calculus as overarching temporal logic and, as
usual, reduce the problem whether $\varphi_1 \equiv \varphi_2$ holds for
contextual formulas $\varphi_1, \varphi_2$ to the problem whether $\varphi_1
\leftrightarrow \varphi_2$ is valid . We show that the problem whether a
contextual formula of the $\mu$-calculus is valid for all contexts can be
reduced to validity of ordinary formulas. Our first result constructs a
canonical context such that a formula is valid for all contexts if{}f it is
valid for this particular one. However, the ordinary formula is exponential in
the nesting-depth of the context variables. In a second result we solve this
problem, thus proving that validity of contextual formulas is EXP-complete, as
for ordinary equivalences. We also prove that both results hold for CTL and LTL
as well. We conclude the paper with some experimental results. In particular,
we use our implementation to automatically prove the correctness of a set of
six contextual equivalences of LTL recently introduced by Esparza et al. for
the normalization of LTL formulas. While Esparza et al. need several pages of
manual proof, our tool only needs milliseconds to do the job and to compute
counterexamples for incorrect variants of the equivalences.
