-> {p : (n : Nat) -> NBush n a -> Set} -> 
           ((x : a) -> p Z x) -> 
           ((n : Nat) -> p (S n) NilB) ->
           ((n : Nat) -> {x : NBush n a} -> {xs : NBush (S (S n)) a} ->
                   p n x -> p (S (S n)) xs -> p (S n) (ConsB x xs)) ->
           (n : Nat) -> (xs : NBush n a) -> p n xs
    indB base nil cons Z xs = base xs
    indB base nil cons (S n) NilB = nil n
    indB base nil cons (S n) (ConsB x xs) =
      cons n (indB base nil cons n x) (indB base nil cons (S (S n)) xs)

Observe that the definition of `indB` is the same as `foldB`, and the type variable `p` is generalized to kind `(n : Nat) -> NBush n a -> Set`. The type of `indB` is specifying how to prove a property `p` holds for any `xs` of type `NBush n a` by induction. More specifically, for the first base case, we need to show `p` holds for any `x` of type `NBush Z a` (which equals `a`), hence 