Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-08 18:07:04 -0700 (Tue, 08 Jul 2008)
Revision: 13100
Log message:

      compiles, runs and even checks up for self-referencial example.
     we still have to check more carefully because proof term and proof are kind of long (see the end of the file)