`p Z x`. For the second base case, we need to show `p` holds for `NilB` of type `NBush (S n) a`. For the step case, we assume `p` holds for `x` of type `NBush n a` and `xs` of type `NBush (S (S n)) a` as the inducton hypotheses, we need to show `p` holds for `ConsB x xs`.

With `indB`, we can now prove properties about `mapB` and `foldB`. In the following we prove that `mapB` has the usual identity and composition properties.

    identity : {a : Set} -> (n : Nat) -> (y : NBush n a) -> y == mapB n (\ x -> x) y
    identity {a} n y =
      indB {a} {\ n v -> v == mapB n (\ x -> x) v} (\ x -> refl)
       (\ n -> refl) (\ n {x} {xs} ih1 ih2 -> cong2 ConsB ih1 ih2) n y

    mapCompose : {a b c : Set} -> (n : Nat) -> (f : b -> c) -> (g : a -> b) ->
     (x : NBush n a) -> mapB n (compose f g) x == mapB n f (mapB n g x)
    mapCompose {a} {b} {c} n 