{a} {p} base step bush 
    uniqueness f hp1 hp2 {a} {p} base step bush = 
      indB {a} {\ n v -> lift n (f base step) v == lift n (hfoldB base step) v} ...

    lift : {a : Set} {p : Set -> Set}
             (n : Nat) -> (g : {a : Set} -> Bush a -> p a) -> NBush n a -> NTimes p n a
    lift {a} {p} Z g x = x
    lift {a} {p} (S n) g x = g (mapB (S Z) (lift {a} {p} n g) x)

The proof of `uniqueness` is nontrivial and requires all the lemmas and theorems about `foldB` and `mapB` we seen so far together with the helper function `lift`. The complete proof can be found in the supplementary material. The key idea of the proof is that instead of proving the concrete theorem `(bush : Bush a) -> f base step bush == hfoldB base step bush`, we use `lift` to prove a more general one, namely, `(n : Nat) -> (bush : NBush n a) -> lift n (f base step) bush == lift n (hfoldB base step) bush`.

The indexed representations {#index}
---------------------------

We now 