Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-29 19:11:38 -0800 (Wed, 29 Mar 2006)
Revision: 8963
Log message:

      In assumption 
         [main] sequent { ...; u: BTerm{'d}; bdepth{'u} = 'd in int; ... >- ... }
       - The second hyp is redundant.
       - The current policy is to avoid the explicit "main" labels.