  We give a new proof of P-time completeness of Linear Lambda Calculus, which
was originally given by H. Mairson in 2003. Our proof uses an essentially
different Boolean type from the type Mairson used. Moreover the correctness of
our proof can be machined-checked using an implementation of Standard ML.
