formalized as the following.


    uniqueness :  (f : {a : Set} -> {p : Set -> Set} -> 
                       ({b : Set} -> p b) -> 
                       ({b : Set} -> b -> p (p b) -> p b) -> Bush a -> p a) ->

                  (hp1 : {a : Set} {p : Set -> Set} -> (base : {b : Set} -> p b) -> 
                         (step : {b : Set} -> b -> p (p b) -> p b) ->
                          f {a} {p} base step NilB == base) ->

                  (hp2 : {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)) ->
                         f base step (ConsB x xs) ==
                         step x (f base step (mapB (S Z) (f base step) xs))) ->

                   {a : Set} -> {p : Set -> Set} ->        
                   (base : {b : Set} -> p b) ->       
                   (step : {b : Set} -> b -> p (p b) -> p b) -> (bush : Bush a) ->       
                   f {a} {p} base step bush == hfoldB 