Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-26 22:35:19 -0800 (Fri, 26 Dec 2003)
Revision: 5217
Log message:
Ext_equal: standard dest_ext_equal and other standard functions added.
Subtype: Elim-style lemmas to prove that subterms are types.
Struct3: replaceWithHypT, replaceWithRevHypT replace "x:T" with "x:S" when "T =e S" in hyps.