theorem :: POLYDIFF:12
(id REAL) `| = REAL --> 1