`ConsB x xs`, we have two induction hypotheses, i.e. `ih1 : x == mapB n ( x -> x) x` and `ih2 : xs == mapB (S (S n)) ( x -> x) xs`. A congruence on these two induction hypotheses, i.e. `cong2 ConsB ih1 ih2`, gives us the proof for `ConsB x xs == mapB (S n) ( x -> x) (ConsB x xs)`. The proof of `mapCompose` is similar to the proof of `identity`.

Recall that Agda does not accept the general recursive definition of `hmapB` in Section \[intro\]. Now that we understand that `hmapB` is just `mapB (S Z)`, we can use the induction principle `indB` to show that `mapB (S Z)` has the same computational behavior as `hmapB`.

    mapNilB : forall {a b : Set} -> (f : a -> b) -> mapB (S Z) f NilB == NilB
    mapNilB {a} {b} f = refl

    mapConsB : {a b : Set} -> (f : a -> b) -> (x : a) -> (xs : Bush (Bush a)) ->
               mapB (S Z) f (ConsB x xs) == ConsB (f x) (mapB (S Z) (mapB (S Z) f) xs)
    mapConsB {a} {b} f x xs = cong (ConsB 