Herbelin presented (at CSL'94) a simple sequent calculus for 
minimal implicational logic, extensible to full first-order 
intuitionistic logic, with a complete system of cut-reduction 
rules which is both confluent and strongly normalising. Some of 
the cut rules may be regarded as rules to construct explicit 
substitutions. He observed that the addition of a cut permutation 
rule, for propagation of such substitutions, breaks the proof of 
strong normalisation; the implicit conjecture is that the rule 
may be added without breaking strong normalisation.  We prove 
this conjecture, thus showing how to model beta-reduction in his 
calculus (extended with rules to allow cut permutations).