λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → ../../../../../Prelude/Natural/fold +3 natural succ zero