λ(r : { a : Natural }) → r with b.c.d = 3