Mechanisation of an elegant proof by Masako Takahashi

This is the first proof in "Parallel Reduction in λ-Calculus" from
Information and Computation 118 (1995).