property `p` in `indB` with ` n v -> v == mapB n ( x -> x) v`. Thus the type of `indB ` is the following.

    ((x : a) -> x == mapB Z (\ x -> x) x) ->
    ((n : Nat) -> NilB == mapB (S n) (\ x -> x) NilB) ->
    ((n : Nat) -> {x : NBush n a} -> {xs : NBush (S (S n)) a} ->
          x == mapB n (\ x -> x) x ->
          xs == mapB (S (S n)) (\ x -> x) xs ->
          ConsB x xs == mapB (S n) (\ x -> x) (ConsB x xs)) ->
    (n : Nat) -> (xs : NBush n a) -> xs == mapB n (\ x -> x) xs  

We need to provide three arguments for `indB ` to obtain a proof of the theorem `(n : Nat) -> (xs : NBush n a) -> xs == mapB n ( x -> x) xs`. These three arguments correspond to the three cases in the inductive proof, i.e. a case for `NBush Z a`, a case for `NilB` and a case for `ConsB x xs`. In the third case for 