Folding left and right over Peano numbers

Abstract

For example, consider the standard powerset function that maps the representation of a set as the list of its elements (in any order and without repetition) to the representation of its powerset:Definition powerset (V : Type) (vs : list V)