Bush a

According to Bird and Meertens [@bird1998nested §1], at each step down the list, entries are *bushed*. For example, a value of type `Bush Nat` can be visualized as the following.


     bush1 = [ 4,                                        -- Nat
               [ 8, [ 5 ], [ [ 3 ] ] ],             -- Bush Nat
               [ [ 7 ], [ ], [ [ [ 7 ] ] ] ], -- Bush (Bush Nat)
               [ [ [ ], [ [ 0 ] ] ] ]  -- Bush (Bush (Bush Nat))
             ]           -- Bush (Bush (Bush (Bush (Bush Nat))))

We can use general recursion to define the following map function and fold function.

    hmapB : {b c : Set} -> (b -> c) -> Bush b -> Bush c
    hmapB f NilB = NilB
    hmapB f (ConsB x xs) = ConsB (f x) (hmapB (hmapB f) xs)

    hfoldB : {a : Set} -> {p : Set -> Set} -> 
              ({b : Set} -> p b) -> ({b : Set} -> b -> p (p b) -> p b) -> Bush a -> p a
    hfoldB base step NilB = base
    hfoldB base step (ConsB x xs) = 
      step x (hfoldB base step (hmapB (hfoldB base 