Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 18:52:00 -0800 (Wed, 01 Mar 2006)
Revision: 8812
Log message:

      Use the labels mechanism instead of the "SelectOption 5" hack to control
      whether the "intensional" wf rules for list operations should be allowed. The
      label that controls these rules is "intensional_wf_option" (prohibited by
      default).
      
      P.S. The intentional wf rules have the form
         l in list --> all_list{l; x. ... } --> ...
      while the extensional ones have the form
         l in A list --> all x: A. ... --> ...