diff --git a/book/src/operations.md b/book/src/operations.md
index 77d5522..2f96c19 100644
--- a/book/src/operations.md
+++ b/book/src/operations.md
@@ -34,7 +34,7 @@ The following table summarizes "syntactic sugar" operations.  These operations a
 | Code | Identifier            | Args and desugaring              | 
 |------|-----------------------|---------------------|
 | 1001 | DictContainsFromEntries | `DictContainsFromEntries(dict_st, key_st, value_st, proof_st) -> ContainsFromEntries(dict_st, key_st, value_st, proof_st)` |
-| 1002 | DictNotContainsFromEntries | `DictNotContainsFromEntries(dict_st, key_st, value_st, proof_st) -> NotContainsFromEntries(dict_st, key_st, value_st, proof_st)` |
+| 1002 | DictNotContainsFromEntries | `DictNotContainsFromEntries(dict_st, key_st, proof_st) -> NotContainsFromEntries(dict_st, key_st, proof_st)` |
 | 1003 | SetContainsFromEntries | `SetContainsFromEntries(set_st, value_st, proof_st) -> ContainsFromEntries(set_st, value_st, value_st, proof_st)` |
 | 1004 | SetNotContainsFromEntries | `SetNotContainsFromEntries(set_st, value_st, proof_st) -> NotContainsFromEntries(set_st, value_st, value_st, proof_st)` |
 | 1005 | ArrayContainsFromEntries | `ArrayContainsFromEntries(array_st, index_st, value_st, proof_st) -> ContainsFromEntries(array_st, index_st, value_st, proof_st)` |
diff --git a/book/src/statements.md b/book/src/statements.md
index d52c00e..f66c283 100644
--- a/book/src/statements.md
+++ b/book/src/statements.md
@@ -49,7 +49,7 @@ The frontend also exposes the following syntactic sugar predicates.  These predi
 | Code | Identifier    | Args and desugaring                | 
 |------|---------------|---------------------|
 | 1000 | DictContains | `DictContains(root, key, val) -> Contains(root, key, val)` |
-| 1001 | DictNotContains | `DictNotContains(root, key, val) -> NotContains(root, key, val)` |
+| 1001 | DictNotContains | `DictNotContains(root, key) -> NotContains(root, key)` |
 | 1002 | SetContains | `SetContains(root, val) -> Contains(root, val, val)` |
 | 1003 | SetNotContains | `SetNotContains(root, val) -> Contains(root, val, val)` |
 | 1004 | ArrayContains | `ArrayContains(root, idx, val) -> Contains(root, idx, val)` |