We present a sequent calculus for formally verifying
modal mu-calculus properties of concurrent processes.
Building on work by Dam and Gurov, the proof system
contains rules for the explicit manipulation of
fixed-point approximants. We develop a new syntax for
approximants, incorporating, in particular, a mechanism
for approximant modification. We make essential use of
this feature to prove our main result: the sequent
calculus is complete for establishing arbitrary
mu-calculus properties of context-free processes.