We prove a folklore theorem, that two derivations in a cut-free
sequent calculus for
intuitionistic propositional logic (based on Kleene's **G3**) are
inter-permutable (using a set of
basic "permutation reduction rules" derived from Kleene's work in 1952) iff
they determine
the same natural deduction. The basic rules form a confluent and weakly
normalising
rewriting system. We refer to Schwichtenberg's proof elsewhere
that a modification of this system is strongly normalising.