n
    foldB base nil cons (S n) (ConsB x xs) = 
      cons n (foldB base nil cons n x) (foldB base nil cons (S (S n)) xs)

The dependently typed fold `foldB` captures the most general form of computing/traversal on the abstract data type `NBush n a`. The definition of `foldB` is well-founded because all the recursive calls of `foldB` are on the components of `ConsB`. Observe that the definition of `foldB` has the same structure as `mapB`. We can redefine `mapB` using `foldB`.

    mapB : {a b : Set} -> (n : Nat) -> (a -> b) -> NBush n a -> NBush n b
    mapB {a} {b} n f l = 
      foldB {a} {\ n -> NBush n b} f (\ n -> NilB) (\ n -> ConsB) n l

The dependently typed fold `foldB` allows us to directly define other terminating functions such as the summation of all the entries in `Bush Nat` and the length function for `Bush`.

    sumB : Bush Nat -> Nat
    sumB = foldB {Nat} {\ n -> Nat} (\ x -> x) (\ n -> Z) (\ n -> add) (S Z) 

    lengthB : {a : Set} -> Bush a -> Nat
    