max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   = 4000
min  #-tests   =  200  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Name
_ :: Prop
False :: Bool
True :: Bool
(==) :: Prop -> Prop -> Bool
eval :: Prop -> Prop
varOf :: Prop -> Name
subst :: Name -> Bool -> Prop -> Prop
taut :: Prop -> Bool
(==) :: Bool -> Bool -> Bool
(==) :: Name -> Name -> Bool

     (p == p) == True
     (p == p) == True
  (p == True) == p
     (n == n) == True
taut (eval p) == taut p
     (p == q) == (q == p)
eval (eval p) == eval p

    p ==> True
False ==> p

p ==> subst n True q == subst n p q