Spec Example 7.11. Plain Implicit Keys