λ(r : { a : Natural }) → r with b = 2