(f x)) (addMap {a} {b} (S Z) f xs)

    addMap : {a b : Set} -> (n : Nat) -> (f : a -> b) -> (x : NBush (add n n) a) ->
              mapB (add n n) f x == mapB n (mapB n f) x
    addMap {a} {b} n f x  = 
      indB {NBush n a} {\ m v -> mapB (add m n) f v == mapB m (mapB n f) v}
           (\ x -> refl) (\ n -> refl) 
           (\ n {x} {xs} ih1 ih2 -> cong2 ConsB ih1 ih2) n x

The theorem `mapNilB` corresponds to the first case in the general recursive definition of `hmapB`, the theorem `mapConsB` corresponds to the second case. To prove `mapConsB`, we need to prove a more general lemma `addMap`. The proof of lemma `addMap` is by standard induction, however, coming up with the correct lemma `addMap` requires some effort.

Similarly, we can use `indB` to show that the `hfoldB` defined from `foldB` behaves the same as the one defined by general recursion. The following theorem `foldBNilB` corresponds to the first case in the general recursive definition, and theorem `foldBConsB` corresponds to the second case. We elide the nontrivial 