proof of the lemma `lemmConsB` (which uses `indB`).

    foldBNilB : {a : Set} -> {p : Set -> Set} -> (base : {b : Set} -> p b) ->
                (step : {b : Set} -> b -> p (p b) -> p b) -> 
                hfoldB {a} {p} base step NilB == base
    foldBNilB base step = refl

    foldBConsB : {a : Set} -> {p : Set -> Set} -> (base : {b : Set} -> p b) ->
                 (step : {b : Set} -> b -> p (p b) -> p b) ->
                 (x : a) -> (xs : Bush (Bush a)) -> 
                 hfoldB base step (ConsB x xs) ==
                 step x (hfoldB base step (mapB (S Z) (hfoldB base step) xs))
    foldBConsB {a} {p} base step x xs = 
      cong (step x) (lemmConsB {a} {p} (S Z) base step xs)

Finally, we use the induction principle `indB` to prove that for any function `f`, if `f` behaves according to `foldBNilB` and `foldBConsB`, i.e. `f base step NilB == base` and `f base step (ConsB x xs) == step x (f base step (mapB (S Z) (f base step) xs)`, then `f` is equal to `hfoldB`. This statement can be 