Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2007-08-31 09:38:15 -0700 (Fri, 31 Aug 2007)
Revision: 12063
Log message:

      1.Coq uses same rules for statements of the form 'T' and 't in T', we had to add some extra rules to support it, which finally brought extracts into the theory.
     2.Added some thinning rules
     3.Added cut rule, we could not find it among Coq rules but there is a tactic which does what assertT does in ITT, so cut has to be in CIC at least in some form
     4.level parameters' arithmetic was not properly done, fixed
     5.added some annotation but we actually need to write a tactic to deduce term types 
     6.Started to work on conjunction, which is defined as a recursive type in CIC