Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-26 12:56:33 -0800 (Sun, 26 Feb 2006)
Revision: 8787
Log message:

      - Changed the definition of the SimpleStep predicate to include the wf
        conditions for the subterms.
      
      - Proved the Itt_hoas_proof_ind.step_union_logic_elim rule.