Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-24 18:49:31 -0800 (Fri, 24 Feb 2006)
Revision: 8785
Log message:

      Some helper lemmas for the elimination proof. Unfortunately the
      step_union_logic_elim rule is not provable as is - we either need a bunch of
      extra wf conditions (which would be unfortunate), or we need to strengthen the
      SimpleStep definition to include those wf conditions (which is my current
      plan).