A proof of the leftmost reduction theorem for λβη-calculus

A new proof of the leftmost reduction theorem for βη-reduction is presented. The proof is carried out directly by using the notion of parallel reduction and without fundamental theorems for λ-calculus.