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)

_ :: 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
     isNode x (addNode x a) == True
     (empty == addNode x a) == False
               isPath x x a == isNode x a
         (a == addNode x a) == isNode x a
                   (x == y) == isNode x (addNode y empty)
 isNode x (addNode y empty) == isNode y (addNode x empty)
          subgraph xs empty == empty
              subgraph [] a == empty
    addNode x (addNode x a) == addNode x a
subgraph xs (subgraph xs a) == subgraph xs a
    addNode x (addNode y a) == addNode y (addNode x a)
subgraph xs (subgraph ys a) == subgraph ys (subgraph xs a)

     isEdge x y a ==> isNode x a
     isEdge x y a ==> isNode y a
     isPath x y a ==> isNode x a
     isPath x y a ==> isNode y a
     isEdge x y a ==> isPath x y a
            empty <=  a
                a <=  addNode x a
    subgraph xs a <=  a
                a <=  addEdge x y a
  addNode x empty <=  addNode x a
      addNode x a <=  addEdge x y a
addEdge x y empty <=  addEdge x y a

isEdge x y a ==>             addEdge x y a == a
   elem x xs ==> subgraph xs (addNode x a) == addNode x (subgraph xs a)