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

_ :: Tril
M :: Tril
F :: Tril
T :: Tril
neg :: Tril -> Tril
(&&&) :: Tril -> Tril -> Tril

p == M

M <= p