show that the nested data type `Bush` is in fact definable even in a core type theory without nested data types. Indeed, we can define `NBush` directly as a non-nested indexed data type `BushN` (called the *indexed representation*). The nested data type `Bush` is recoverable as `BushN (S Z)`. This opens the possibility of a user defined nested data type in a surface language, then it can be automatically desugared to a non-nested definition in the underlying type theory while still providing the fold function and induction principle. For example, the total dependently typed language Coq does not accept nested data types such as `Bush` due to the failure of Coq’s strict positivity check. So in this case we can work with the indexed representations instead.

Consider the following indexed data type `BushN`.

    data BushN : Nat -> Set -> Set where
      Base : {a : Set} -> a -> BushN Z a
      NilBN : {a : Set} -> {n : Nat} -> BushN (S n) a
      ConsBN : {a : Set} -> {n : Nat} -> 
                BushN n a -> BushN (S (S n)) a -> BushN (S n) a

The `BushN` data type is indexed by the natural 