f g x =
      indB {a} {\ n v -> mapB n (compose f g) v == mapB n f (mapB n g v)}
       (\ v -> refl) (\ n -> refl) (\ n {x1} {xs} ih1 ih2 -> cong2 ConsB ih1 ih2) n x

    cong2 : {a b c : Set} -> {m1 n1 : a} -> {m2 n2 : b} -> 
             (f : a -> b -> c) -> m1 == n1 -> m2 == n2  -> f m1 m2 == f n1 n2

We note that the usual way of proving things in Agda is by recursion, and relying on the Agda termination checker to prove termination. However, since our purpose is to show the strength of induction principles such as `indB`, we do not use recursion at all. All the proofs in this paper are by induction principles.

Let us take a closer look at `identity`. It is a general statement of `mapB n` (includes the special case `mapB (S Z)`). It is also about a property of `y : NBush n a`, i.e. `y` has the property of being equal to `mapB n ( x -> x) y` for any `n`. So we instantiate the 