λ(f : ∀(natural : Type) → (natural → natural) → natural → natural)
→ f Natural (λ(x : Natural) → x + 1) 0