Mechanisation of an elegant proof by Masako Takahashi This is the first proof in "Parallel Reduction in λ-Calculus" from Information and Computation 118 (1995).