max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   =   30
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Symbol
_ :: RE Symbol
Empty :: RE Symbol
None :: RE Symbol
Star :: RE Symbol -> RE Symbol
(:+) :: RE Symbol -> RE Symbol -> RE Symbol
(:.) :: RE Symbol -> RE Symbol -> RE Symbol
(<=) :: RE Symbol -> RE Symbol -> Bool
(==) :: RE Symbol -> RE Symbol -> Bool
False :: Bool
True :: Bool

     (r <= Empty) == True
      (None <= r) == True
    (r <= Star s) == True
 (Star r <= None) == False
     (r == Empty) == (Empty <= r)
      (r == None) == (r <= None)
    (r == Star s) == (Star s <= r)
           r :+ r == r
        r :+ None == r
       r :. Empty == r
        r :. None == None
    Star (Star r) == Star r
           r :+ s == s :+ r
           r :. s == s :. r
      r :+ Star r == Star r
Star (r :+ Empty) == Star r
  Empty :+ Star r == Star r

 r <= None ==> r <= s
      None <=  r
         r <=  Star r
     Empty <=  Star r
         r <=  r :+ s
    r :. r <=  Star r
r :+ Empty <=  Star r
    r :. s <=  r :+ s