Dyckhoff and Pinto present a weakly normalising system of reductions on derivations in the cut-free intuitionistic sequent calculus, where the normal derivations are characterised as the fixed points of the composition of the Prawitz translations into natural deduction and back. This paper presents a formalisation of the system, including a proof of the weak normalisation property for the formalisation. More details can be found in earlier work by the author. The formalisation has been kept as close as possible to the original presentation to allow an evaluation of the state of proof assistance for such methods, and to ensure similarity of methods, and not merely similarity of results. The formalisation is restricted to the implicational fragment of intuitionistic logic.