Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-14 19:07:58 -0700 (Mon, 14 Jul 2008)
Revision: 13122
Log message:

      Added Nec rule, in its generic (not restricted to axioms) form.
     As a result, deduction theorem has to consider two cases - hyps-free and non-hyp-free but for an axiom. May, be it would be more straightforward to use axiom-nly Nec.
     But for now we follow Artemov's TCS paper.