lemma may be easier than proving a concrete one. We will use this principle again and again when verifying programs involving nested data types.

From now on, instead of considering the concrete data type `Bush`, we will focus on its generalized counterpart `NBush n`. Looking at the definition of `mapB`, we can view `NBush n` as a kind of abstract indexed data type that has three constructors. The first constructor has type `a -> NBush Z a`, corresponding to the first case of `mapB`. The second constructor `NilB` has type `NBush (S n) a`, and the third constructor `ConsB` has type `NBush n a -> NBush (S (S n)) a -> NBush (S n) a`.

We now give the following dependently typed fold for the abstract indexed data type `NBush n`.

    foldB : {a : Set} -> {p : Nat -> Set} ->
            (a -> p Z) ->
            ((n : Nat) -> p (S n)) ->
            ((n : Nat) -> p n -> p (S (S n)) -> p (S n)) ->
            (n : Nat) -> NBush n a -> p n
    foldB base nil cons Z x = base x
    foldB base nil cons (S n) NilB = nil 