Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 15:47:58 -0800 (Fri, 17 Feb 2006)
Revision: 8726
Log message:

      Now that the squash is a defined operator and not a postulated one, I am a bit
      uncomfortable using it in the esquash axioms. The problem is that definitions
      tend to change once in a while and it's better not to have to rely on a them
      not changing in a way that would invalidate the seemingly unrelated axioms.
      
      This changes the equash axioms slightly, so that they do not refer to squash
      operator and the rules squash-related rule are now all derived.
      
      Alexei Kopylov have reviewed the changes to esquash axioms.