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

_ :: Bool
_ :: Nat
_ :: Digraph Nat
_ :: [Nat]
[] :: [Nat]
elem :: Nat -> [Nat] -> Bool
empty :: Digraph Nat
addNode :: Nat -> Digraph Nat -> Digraph Nat
addEdge :: Nat -> Nat -> Digraph Nat -> Digraph Nat
isNode :: Nat -> Digraph Nat -> Bool
isEdge :: Nat -> Nat -> Digraph Nat -> Bool
isPath :: Nat -> Nat -> Digraph Nat -> Bool
subgraph :: [Nat] -> Digraph Nat -> Digraph Nat
True :: Bool
False :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Nat -> Nat -> Bool
(==) :: Digraph Nat -> Digraph Nat -> Bool
(==) :: [Nat] -> [Nat] -> Bool

   isNode x empty == False
 isEdge x y empty == False
 isPath x y empty == False
     isPath x x a == isNode x a
subgraph xs empty == empty
    subgraph [] a == empty

          empty <= a
              a <= addNode x a
  subgraph xs a <= a
addNode x empty <= addNode x a

isNode x a ==> addNode x a == a