diff --git a/Makefile b/Makefile
index f915ad35..46ec8f7a 100644
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,7 @@
 MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 default: build exercises build/tutorial.html build/exercises.zip
+all: default
 
 clean:
 	rm -rf build TAGS
@@ -43,6 +44,10 @@ build/solutions/%: src/examples/%
 build/exercises.zip: $(EXERCISES)
 	cd build; zip -r exercises.zip exercises > /dev/null
 
+WORKING=$(wildcard src/examples/list_*.c)
+WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING))
+temp: $(WORKING_AUX) build 
+#     build/tutorial.html 
 
 ##############################################################################
 # Check that the examples all run correctly 
diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md
new file mode 100644
index 00000000..01a64f69
--- /dev/null
+++ b/NAMING-CONVENTIONS.md
@@ -0,0 +1,139 @@
+CN Naming Conventions
+---------------------
+
+This document describes our (Benjamin and Liz's) current best shot at
+a good set of conventions for naming identifiers in CN, based on
+numerous discussions and worked examples.
+
+All the list-related files in src/examples have been converted to this
+convention -- do `ls src/examples/list*` to check it out.
+
+# Principles
+
+- When similar concepts exist in both C and CN, they should be named
+  so that the correspondence is immediately obvious.
+     - In particular, the C and CN versions of a given data structure
+       should have very similar names.
+
+- In text, we use the modifiers _CN-level_ vs. _C-level_ to
+  distinguish the two worlds.
+
+# General conventions
+
+ ## For new code
+
+When we're writing both C and CN code from scratch (e.g., in the
+tutorial), we aim for maximal correspondence between 
+
+- In general, CN identifiers are written in `snake_case` rather than `camlCase`
+
+- C-level identifiers are `lowercase_consistently_throughout`
+
+- CN-level identifiers are `Uppercase_Consistently_Throughout`
+
+- A CN identifier that represents the state of a mutable data
+  structure after some function returns should be named the same as
+  the starting state of the data structure, with an `_post` at the
+  end.
+      - E.g., The list copy function takes a linked list `l`
+        representing a sequence `L` and leaves `l` at the end pointing
+        to a final sequence `L_post` such that `L == L_post`.
+        (Moreover, it returns a new sequence `Ret` with `L == Ret`.)
+
+- Predicates that extract some structure from the heap should be named
+  the same as the structure they extract.  E.g., the result
+  type of the `Queue` predicate is also called `Queue`.
+
+  *Discussion*: There is clearly some potential for confusion, and for
+  this reason Liz prefers using `Queue_at` for the predicate.  On the
+  other hand hand, types don't take an argument and predicates do, so
+  it's easy to disambiguate.  We're going with the lighter alternative
+  for the moment.
+  
+## For existing code
+
+In existing C codebases, uppercase-initial identifiers are often used
+for typedefs, structs, and enumerations.  We should choose a
+recommended standard convention for such cases -- e.g., "prefix
+CN-level identifiers with `CN` when needed to avoid confusion with
+C-level identifiers".  Some experimentation will be needed to see
+which convention we like best; this is left for future discussions.
+
+# Built-ins
+
+This proposal may also require changing some built-ins for
+consistency.
+
+      - `i32` should change to `I32`, `u64` to `U64`
+      - `is_null` to `Is_null` (or `Is_Null`)
+
+*Discussion*: One point against this change is that CN currently tries
+to use names reminiscent of Rust (`i32`, `u64`, etc.).  I (BCP) do not
+personally find this argument persuasive -- internal consistency seems
+more important than miscellaeous points of similarity with some other
+language.  One way or the other, this will require a global decision.
+
+# Polymorphism
+
+One particularly tricky issue is how to name the "monomorphic
+instances" of "morally polymorphic" functions (i.e., whether to write
+`append__Int` or `append__List_Int` rather than just `append`).  On
+one hand, `append__Int` is "more correct".  On the other hand, these
+extra annotations can get pretty heavy.
+
+We propose a compromise:
+
+1. If a project needs to use two or more instances of some polymorphic
+   type, then the names of the C and CN types, the C and CN functions
+   operating over them, and the CN predicates describing them are all
+   suffixed with `__xxx`, where `xxx` is the appropriate "type
+   argument".  E.g., if some codebase uses lists of both signed and
+   unsigned 32-bit ints, then we would use names like this:
+      - `list__int` / `list__uint`
+      - `append__int` / `append__uint`
+      - `List__I32` / `List__U32`
+      - `Cons__I32` / `Cons__U32`
+      - etc.
+
+2. However, if, in a given project, a set of "morally polymorphic"
+   type definitions and library functions is *only used at one
+   monomorphic instance* (e.g., if some codebase only ever uses lists
+   of 32-bit signed ints), then the `__int` or `__I32` annotations are
+   omitted.
+
+   This convention is used in the CN tutorial, for example.
+
+   TODO: Right now, the tutorial uses option (1).  It was this
+   exercise that convinced me [BCP] that option (2) was better. :-)
+
+*Discussion*: One downside of this convention is that it might
+sometimes require some after-the-fact renaming: If a project starts
+out using just lists of signed ints and later needs to introduce lists
+of unsigned ints, the old signed operations will need to be renamed.
+This seems like an acceptable cost for keeping things light.
+
+Another downside is that it introduces two different ways of naming
+polymorphic things.  But hopefully (a) the appropriate use of each is
+clear and (b) most C developments will actually fall in the second,
+lighter case, and programmers will never need to bother understanding
+the first case.
+
+# Loose ends
+
+- Do we need a convention for auxiliary predicates?
+    - E.g., maybe adding `_Aux` to the original predicate name
+      (e.g. `Queue_Aux` for the recursive predicate that walks down
+      the list of queue nodes to gather them into a list once a
+      top-level `Queue` or `Queue_at` predicate has dealt with the
+      non-recursive part of the structure).
+
+- The current function `IntList_free__list` is hard to rename with
+  these conventions. It feels like it should be `free__sllist`, but
+  that’s also the new name of the free function for individual list
+  cells (opposite of `malloc`). Current solution is
+  `free_rec__sllist`.
+    - BCP wonders if this issue is specific to malloc and free.  If
+      so, maybe we can make some special convention like
+      `free__sllist_node` for the single-node operation (even though
+      what it returns is an `sllist`, noit an `sllist_node`),
+      leaving `free__sllist` for the recursive one?
diff --git a/src/example-archive/simple-examples/working/malloc_1.c b/src/example-archive/simple-examples/working/malloc_1.c
index cd837ed7..9259c221 100644
--- a/src/example-archive/simple-examples/working/malloc_1.c
+++ b/src/example-archive/simple-examples/working/malloc_1.c
@@ -3,19 +3,19 @@
 // malloc() is not defined by default in CN. We can define a fake malloc()
 // function that only works on ints.
 
-int *my_malloc_int()
+int *my_malloc__int()
 /*@ trusted; @*/
 /*@ ensures take New = Block<int>(return); @*/
 {}
 
-int *malloc_1()
+int *malloc__1()
 /*@ ensures 
       take New = Owned<int>(return);
       New == 7i32;
       *return == 7i32; @*/  // <-- Alternative syntax 
 {
   int *new;
-  new = my_malloc_int();
+  new = my_malloc__int();
   *new = 7; // Have to initialize the memory before it's owned
   return new;
 }
diff --git a/src/examples/Dbl_Linked_List/add.c b/src/examples/Dbl_Linked_List/add.c
index b988d9a4..b6efc54a 100644
--- a/src/examples/Dbl_Linked_List/add.c
+++ b/src/examples/Dbl_Linked_List/add.c
@@ -5,11 +5,11 @@ struct node *add(int element, struct node *n)
 /*@ requires take Before = Dll_at(n);
     ensures  take After = Dll_at(return);
 
-             is_null(n) ? After == Dll { left: Seq_Nil{}, curr: Node(After), right: Seq_Nil{}}
-                        : After == Dll { left: Seq_Cons{head: Node(Before).data, tail: Left(Before)}, curr: Node(After), right: Right(Before)};
+             is_null(n) ? After == Dll { left: Nil{}, curr: Node(After), right: Nil{}}
+                        : After == Dll { left: Cons{Head: Node(Before).data, Tail: Left(Before)}, curr: Node(After), right: Right(Before)};
 @*/
 {
-    struct node *new_node = malloc_node();
+    struct node *new_node = malloc__node();
     new_node->data = element;
     new_node->prev = 0;
     new_node->next = 0;
diff --git a/src/examples/Dbl_Linked_List/add_orig.broken.c b/src/examples/Dbl_Linked_List/add_orig.broken.c
index f8b9b306..0d60e519 100644
--- a/src/examples/Dbl_Linked_List/add_orig.broken.c
+++ b/src/examples/Dbl_Linked_List/add_orig.broken.c
@@ -3,7 +3,7 @@
 // Adds after the given node and returns a pointer to the new node
 struct node *add(int element, struct node *n)
 {
-    struct node *new_node = malloc_node();
+    struct node *new_node = malloc__node();
     new_node->data = element;
     new_node->prev = 0;
     new_node->next = 0;
diff --git a/src/examples/Dbl_Linked_List/cn_types.h b/src/examples/Dbl_Linked_List/cn_types.h
index 59278fb2..e82cf9fd 100644
--- a/src/examples/Dbl_Linked_List/cn_types.h
+++ b/src/examples/Dbl_Linked_List/cn_types.h
@@ -1,6 +1,6 @@
 /*@
 datatype Dll {
     Empty_Dll {},
-    Dll {datatype seq left, struct node curr, datatype seq right}
+    Dll {datatype List left, struct node curr, datatype List right}
 }
 @*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/getters.h b/src/examples/Dbl_Linked_List/getters.h
index 9e180623..ff54d2d7 100644
--- a/src/examples/Dbl_Linked_List/getters.h
+++ b/src/examples/Dbl_Linked_List/getters.h
@@ -1,14 +1,14 @@
 /*@
-function (datatype seq) Right (datatype Dll L) {
+function (datatype List) Right (datatype Dll L) {
     match L {
-        Empty_Dll {} => { Seq_Nil{} }
+        Empty_Dll {} => { Nil{} }
         Dll {left: _, curr: _, right: r} => { r }
     }
 }
 
-function (datatype seq) Left (datatype Dll L) {
+function (datatype List) Left (datatype Dll L) {
     match L {
-        Empty_Dll {} => { Seq_Nil {} }
+        Empty_Dll {} => { Nil {} }
         Dll {left: l, curr: _, right: _} => { l }
     }
 }
diff --git a/src/examples/Dbl_Linked_List/malloc_free.h b/src/examples/Dbl_Linked_List/malloc_free.h
index 1937a5a3..c03dc804 100644
--- a/src/examples/Dbl_Linked_List/malloc_free.h
+++ b/src/examples/Dbl_Linked_List/malloc_free.h
@@ -1,12 +1,12 @@
-extern struct node *malloc_node();
-/*@ spec malloc_node();
+extern struct node *malloc__node();
+/*@ spec malloc__node();
     requires true;
     ensures take u = Block<struct node>(return);
             !ptr_eq(return,NULL);
 @*/ 
 
-extern void free_node (struct node *p);
-/*@ spec free_node(pointer p);
+extern void free__node (struct node *p);
+/*@ spec free__node(pointer p);
     requires take u = Block<struct node>(p);
     ensures true;
 @*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/node_and_int.h b/src/examples/Dbl_Linked_List/node_and_int.h
index faef87c7..dd223296 100644
--- a/src/examples/Dbl_Linked_List/node_and_int.h
+++ b/src/examples/Dbl_Linked_List/node_and_int.h
@@ -3,15 +3,15 @@ struct node_and_int {
   int data;
 };
 
-extern struct node_and_int *malloc_node_and_int();
-/*@ spec malloc_node_and_int();
+extern struct node_and_int *malloc__node_and_int();
+/*@ spec malloc__node_and_int();
     requires true;
     ensures take u = Block<struct node_and_int>(return);
             !ptr_eq(return,NULL);
 @*/ 
 
-extern void free_node_and_int (struct node_and_int *p);
-/*@ spec free_node_and_int(pointer p);
+extern void free__node_and_int (struct node_and_int *p);
+/*@ spec free__node_and_int(pointer p);
     requires take u = Block<struct node_and_int>(p);
     ensures true;
 @*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/predicates.h b/src/examples/Dbl_Linked_List/predicates.h
index a5353591..c5c4d54a 100644
--- a/src/examples/Dbl_Linked_List/predicates.h
+++ b/src/examples/Dbl_Linked_List/predicates.h
@@ -10,27 +10,27 @@ predicate (datatype Dll) Dll_at (pointer p) {
     }
 }
 
-predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) {
+predicate (datatype List) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) {
     if (is_null(p)) {
-        return Seq_Nil{};
+        return Nil{};
     } else {
         take n = Owned<struct node>(p);
         assert (ptr_eq(n.prev, prev_pointer));
         assert(ptr_eq(prev_node.next, p));
         take Right = Own_Forwards(n.next, p, n);
-        return Seq_Cons{head: n.data, tail: Right};
+        return Cons{Head: n.data, Tail: Right};
     }
 }
 
-predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) {
+predicate (datatype List) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) {
     if (is_null(p)) {
-        return Seq_Nil{};
+        return Nil{};
     } else {
         take n = Owned<struct node>(p);
         assert (ptr_eq(n.next, next_pointer));
         assert(ptr_eq(next_node.prev, p));
         take Left = Own_Backwards(n.prev, p, n);
-        return Seq_Cons{head: n.data, tail: Left};
+        return Cons{Head: n.data, Tail: Left};
     }
 }
 @*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/remove.c b/src/examples/Dbl_Linked_List/remove.c
index 2a610db8..18a8c361 100644
--- a/src/examples/Dbl_Linked_List/remove.c
+++ b/src/examples/Dbl_Linked_List/remove.c
@@ -11,8 +11,8 @@ struct node_and_int *remove(struct node *n)
              take After = Dll_at(ret.node);
              ret.data == del.data;
              (is_null(del.prev) && is_null(del.next)) ? After == Empty_Dll{}
-                 : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: tl(Right(Before))}
-                     : After == Dll{left: tl(Left(Before)), curr: Node(After), right: Right(Before)});
+                 : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: Tl(Right(Before))}
+                     : After == Dll{left: Tl(Left(Before)), curr: Node(After), right: Right(Before)});
 @*/
 {
     struct node *temp = 0;
@@ -27,10 +27,10 @@ struct node_and_int *remove(struct node *n)
         temp = n->next;
     }
 
-    struct node_and_int *pair = malloc_node_and_int();
+    struct node_and_int *pair = malloc__node_and_int();
     pair->node = temp;
     pair->data = n->data;
 
-    free_node(n);       
+    free__node(n);       
     return pair;
 }
diff --git a/src/examples/Dbl_Linked_List/remove_orig.broken.c b/src/examples/Dbl_Linked_List/remove_orig.broken.c
index b2617c69..5a4b8b24 100644
--- a/src/examples/Dbl_Linked_List/remove_orig.broken.c
+++ b/src/examples/Dbl_Linked_List/remove_orig.broken.c
@@ -15,10 +15,10 @@ struct node_and_int *remove(struct node *n)
         temp = n->next;
     }
 
-    struct node_and_int *pair = malloc_node_and_int();
+    struct node_and_int *pair = malloc__node_and_int();
     pair->node = temp;
     pair->data = n->data;
 
-    free_node(n);       
+    free__node(n);       
     return pair;
 }
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/singleton.c b/src/examples/Dbl_Linked_List/singleton.c
index 15c8fd8a..008daadb 100644
--- a/src/examples/Dbl_Linked_List/singleton.c
+++ b/src/examples/Dbl_Linked_List/singleton.c
@@ -2,10 +2,10 @@
 
 struct node *singleton(int element)
 /*@ ensures take Ret = Dll_at(return);
-        Ret == Dll{left: Seq_Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Seq_Nil{}};
+        Ret == Dll{left: Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Nil{}};
 @*/
 {
-   struct node *n = malloc_node();
+   struct node *n = malloc__node();
    n->data = element;
    n->prev = 0;
    n->next = 0;
diff --git a/src/examples/abs.c b/src/examples/abs.c
index 206ee580..79da4d60 100644
--- a/src/examples/abs.c
+++ b/src/examples/abs.c
@@ -7,8 +7,7 @@ int abs (int x)
 {
   if (x >= 0) {
     return x;
-  }
-  else {
+  } else {
     return -x;
   }
 }
diff --git a/src/examples/abs_mem.c b/src/examples/abs_mem.c
index 488c2992..978fefa0 100644
--- a/src/examples/abs_mem.c
+++ b/src/examples/abs_mem.c
@@ -2,8 +2,8 @@ int abs_mem (int *p)
 /* --BEGIN-- */
 /*@ requires take x = Owned<int>(p);
              MINi32() < x;
-    ensures take x2 = Owned<int>(p);
-            x == x2;
+    ensures take x_post = Owned<int>(p);
+            x == x_post;
             return == ((x >= 0i32) ? x : (0i32-x));
 @*/
 /* --END-- */
diff --git a/src/examples/add_0.c b/src/examples/add_0.c
index 56a35cfd..f0f52745 100644
--- a/src/examples/add_0.c
+++ b/src/examples/add_0.c
@@ -1,7 +1,7 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             -2147483648i64 <= sum; sum <= 2147483647i64; @*/
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64; @*/
 /* --END-- */
 {
   return x+y;
diff --git a/src/examples/add_1.c b/src/examples/add_1.c
index ebd141df..ac30ccc5 100644
--- a/src/examples/add_1.c
+++ b/src/examples/add_1.c
@@ -1,8 +1,8 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             -2147483648i64 <= sum; sum <= 2147483647i64;
-    ensures return == (i32) sum;
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64;
+    ensures return == (i32) Sum;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/add_2.c b/src/examples/add_2.c
index 17339707..0afd69e0 100644
--- a/src/examples/add_2.c
+++ b/src/examples/add_2.c
@@ -1,8 +1,8 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             (i64)MINi32() <= sum; sum <= (i64)MAXi32();
-    ensures return == (i32) sum;
+/*@ requires let Sum = (i64) x + (i64) y;
+             (i64)MINi32() <= Sum; Sum <= (i64)MAXi32();
+    ensures return == (i32) Sum;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/add_read.c b/src/examples/add_read.c
index c15c6484..2341bd04 100644
--- a/src/examples/add_read.c
+++ b/src/examples/add_read.c
@@ -1,10 +1,10 @@
 unsigned int add (unsigned int *p, unsigned int *q)
-/*@ requires take m = Owned<unsigned int>(p);
-             take n = Owned<unsigned int>(q);
-    ensures take m2 = Owned<unsigned int>(p);
-            take n2 = Owned<unsigned int>(q);
-            m == m2 && n == n2;
-            return == m + n;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P == P_post && Q == Q_post;
+            return == P + Q;
 @*/
 {
   unsigned int m = *p;
diff --git a/src/examples/add_two_array.c b/src/examples/add_two_array.c
index 799edaf7..70a8e5fc 100644
--- a/src/examples/add_two_array.c
+++ b/src/examples/add_two_array.c
@@ -1,12 +1,14 @@
 unsigned int array_read_two (unsigned int *p, int n, int i, int j)
 /* --BEGIN-- */
-/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+/*@ requires take A = each(i32 k; 0i32 <= k && k < n) { 
+                        Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
              0i32 <= i && i < n;
              0i32 <= j && j < n;
              j != i;
-    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
-            a1 == a2;
-            return == a1[i] + a1[j];
+    ensures take A_post = each(i32 k; 0i32 <= k && k < n) { 
+                            Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+            A == A_post;
+            return == A[i] + A[j];
 @*/
 /* --END-- */
 {
diff --git a/src/examples/append.c b/src/examples/append.c
index ff3309a0..0b398fb9 100644
--- a/src/examples/append.c
+++ b/src/examples/append.c
@@ -1,18 +1,18 @@
 #include "list.h"
 #include "list_append.h"
 
-struct int_list* IntList_append(struct int_list* xs, struct int_list* ys)
-/*@ requires take L1 = IntList(xs); @*/
-/*@ requires take L2 = IntList(ys); @*/
-/*@ ensures take L3 = IntList(return); @*/
-/*@ ensures L3 == append(L1, L2); @*/
+struct sllist* IntList_append(struct sllist* xs, struct sllist* ys)
+/*@ requires take L1 = SLList(xs);
+             take L2 = SLList(ys); @*/
+/*@ ensures take L3 = SLList(return);
+            L3 == Append(L1, L2); @*/
 {
   if (xs == 0) {
-    /*@ unfold append(L1, L2); @*/
+    /*@ unfold Append(L1, L2); @*/
     return ys;
   } else {
-    /*@ unfold append(L1, L2); @*/
-    struct int_list *new_tail = IntList_append(xs->tail, ys);
+    /*@ unfold Append(L1, L2); @*/
+    struct sllist *new_tail = IntList_append(xs->tail, ys);
     xs->tail = new_tail;
     return xs;
   }
diff --git a/src/examples/append2.c b/src/examples/append2.c
index a966e428..5ea0ac97 100644
--- a/src/examples/append2.c
+++ b/src/examples/append2.c
@@ -1,44 +1,44 @@
 #include "list.h"
 #include "list_append.h"
 
-struct int_list* IntList_copy (struct int_list *xs)
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            take L2 = IntList(return);
-            L1 == L1_;
-            L1 == L2;
+struct sllist* IntList_copy (struct sllist *xs)
+/*@ requires take Xs = SLList(xs);
+    ensures take Xs_post = SLList(xs);
+            take R = SLList(return);
+            Xs == Xs_post;
+            Xs == R;
 @*/
 {
   if (xs == 0) {
-    return IntList_nil();
+    return slnil();
   } else {
-    struct int_list *new_tail = IntList_copy(xs->tail);
-    return IntList_cons(xs->head, new_tail);
+    struct sllist *new_tail = IntList_copy(xs->tail);
+    return slcons(xs->head, new_tail);
   }
 }
 
-struct int_list* IntList_append2 (struct int_list *xs, struct int_list *ys)
+struct sllist* IntList_append2 (struct sllist *xs, struct sllist *ys)
 /* --BEGIN-- */
-/*@ requires take L1 = IntList(xs); @*/
-/*@ requires take L2 = IntList(ys); @*/
-/*@ ensures take L1_ = IntList(xs); @*/
-/*@ ensures take L2_ = IntList(ys); @*/
-/*@ ensures take L3 = IntList(return); @*/
-/*@ ensures L3 == append(L1, L2); @*/
-/*@ ensures L1 == L1_; @*/
-/*@ ensures L2 == L2_; @*/
+/*@ requires take Xs = SLList(xs); @*/
+/*@ requires take Ys = SLList(ys); @*/
+/*@ ensures take Xs_post = SLList(xs); @*/
+/*@ ensures take Ys_post = SLList(ys); @*/
+/*@ ensures take Ret = SLList(return); @*/
+/*@ ensures Ret == Append(Xs, Ys); @*/
+/*@ ensures Xs == Xs_post; @*/
+/*@ ensures Ys == Ys_post; @*/
 /* --END-- */
 {
   if (xs == 0) {
 /* --BEGIN-- */
-    /*@ unfold append(L1, L2); @*/
+    /*@ unfold Append(Xs, Ys); @*/
 /* --END-- */
     return IntList_copy(ys);
   } else {
 /* --BEGIN-- */
-    /*@ unfold append(L1, L2); @*/
+    /*@ unfold Append(Xs, Ys); @*/
 /* --END-- */
-    struct int_list *new_tail = IntList_append2(xs->tail, ys);
-    return IntList_cons(xs->head, new_tail);
+    struct sllist *new_tail = IntList_append2(xs->tail, ys);
+    return slcons(xs->head, new_tail);
   }
 }
diff --git a/src/examples/array_load.broken.c b/src/examples/array_load.broken.c
index 3f4b6e63..446072cf 100644
--- a/src/examples/array_load.broken.c
+++ b/src/examples/array_load.broken.c
@@ -1,7 +1,10 @@
 int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) };
              0i32 <= i && i < n; 
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }; @*/
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) }; 
+@*/
 {
   return p[i];
 }
diff --git a/src/examples/array_load.c b/src/examples/array_load.c
index eef0dab2..6cd87216 100644
--- a/src/examples/array_load.c
+++ b/src/examples/array_load.c
@@ -1,9 +1,10 @@
 int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { 
-                          Owned<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n;
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { 
-                            Owned<int>(array_shift<int>(p,j)) }; @*/
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) };
+             0i32 <= i && i < n; 
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) }; 
+@*/
 {
   /*@ extract Owned<int>, i; @*/
   return p[i];
diff --git a/src/examples/free.h b/src/examples/free.h
index 9643f4f3..b5eb5832 100644
--- a/src/examples/free.h
+++ b/src/examples/free.h
@@ -1,13 +1,13 @@
 extern void freeInt (int *p);
 /*@ spec freeInt(pointer p);
-    requires take v = Block<int>(p);
+    requires take P = Block<int>(p);
     ensures true;
 @*/
 
 
 extern void freeUnsignedInt (unsigned int *p);
 /*@ spec freeUnsignedInt(pointer p);
-    requires take v = Block<unsigned int>(p);
+    requires take P = Block<unsigned int>(p);
     ensures true;
 @*/
 
diff --git a/src/examples/init_array.c b/src/examples/init_array.c
index 5fb3c97a..b288cb1c 100644
--- a/src/examples/init_array.c
+++ b/src/examples/init_array.c
@@ -1,13 +1,17 @@
 void init_array (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+/*@ requires take A = each(u32 i; i < n) { 
+                         Owned<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take ai = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
-          {p} unchanged; {n} unchanged;
+  /*@ inv take Ai = each(u32 i; i < n) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          {p} unchanged; 
+          {n} unchanged;
   @*/
 /* --END-- */
   {
diff --git a/src/examples/init_array2.c b/src/examples/init_array2.c
index e1217845..f447f553 100644
--- a/src/examples/init_array2.c
+++ b/src/examples/init_array2.c
@@ -1,13 +1,17 @@
 void init_array2 (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Block<char>( array_shift<char>(p, i)) };
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+/*@ requires take A = each(u32 i; i < n) { 
+                        Block<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take al = each(u32 i; i < j) { Owned<char>( array_shift<char>(p, i)) };
-          take ar = each(u32 i; j <= i && i < n) { Block<char>( array_shift<char>(p, i)) };
+  /*@ inv take Al = each(u32 i; i < j) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          take Ar = each(u32 i; j <= i && i < n) { 
+                      Block<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           j <= n;
   @*/
diff --git a/src/examples/init_array_rev.c b/src/examples/init_array_rev.c
index dd8de2b7..e46b4f3f 100644
--- a/src/examples/init_array_rev.c
+++ b/src/examples/init_array_rev.c
@@ -1,14 +1,18 @@
-void init_array2 (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Block<char>( array_shift<char>(p, i)) };
+void init_array_rev (char *p, unsigned int n)
+/*@ requires take A = each(u32 i; i < n) { 
+                        Block<char>( array_shift<char>(p, i)) };
     n > 0u32;
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take al = each(u32 i; i < n-j) { Block<char>( array_shift<char>(p, i)) };
-          take ar = each(u32 i; n-j <= i && i < n) { Owned<char>( array_shift<char>(p, i)) };
+  /*@ inv take Al = each(u32 i; i < n-j) { 
+                      Block<char>( array_shift<char>(p, i)) };
+          take Ar = each(u32 i; n-j <= i && i < n) { 
+                      Owned<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           0u32 <= j && j <= n;
   @*/
diff --git a/src/examples/init_point.c b/src/examples/init_point.c
index b907a950..4ecb67f3 100644
--- a/src/examples/init_point.c
+++ b/src/examples/init_point.c
@@ -1,18 +1,18 @@
-void zero (int *p) 
-/*@ requires take u = Block<int>(p);
-    ensures take v = Owned<int>(p);
-            v == 0i32; @*/
+void zero (int *coord) 
+/*@ requires take Coord = Block<int>(coord);
+    ensures take Coord_post = Owned<int>(coord);
+            Coord_post == 0i32; @*/
 {
-  *p = 0;
+  *coord = 0;
 }
 
 struct point { int x; int y; };
 
 void init_point(struct point *p) 
-/*@ requires take s = Block<struct point>(p);
-    ensures take s2 = Owned<struct point>(p);
-            s2.x == 0i32;
-            s2.y == 0i32;
+/*@ requires take P = Block<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == 0i32;
+            P_post.y == 0i32;
 @*/
 {
   zero(&p->x);
diff --git a/src/examples/list.h b/src/examples/list.h
index d93830dc..f3a8238f 100644
--- a/src/examples/list.h
+++ b/src/examples/list.h
@@ -6,4 +6,4 @@
 #include "list_hdtl.h"
 #include "list_constructors.h"
 
-#endif //_LIST_H
+#endif //_LIST_H
\ No newline at end of file
diff --git a/src/examples/list_append.h b/src/examples/list_append.h
index d6305abb..2c95a823 100644
--- a/src/examples/list_append.h
+++ b/src/examples/list_append.h
@@ -1,13 +1,11 @@
-// append.h
-
 /*@
-function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
-  match xs {
-    Seq_Nil {} => {
-      ys
+function [rec] (datatype List) Append(datatype List L1, datatype List L2) {
+  match L1 {
+    Nil {} => {
+      L2
     }
-    Seq_Cons {head : h, tail : zs}  => {
-      Seq_Cons {head: h, tail: append(zs, ys)}
+    Cons {Head : H, Tail : T}  => {
+      Cons {Head: H, Tail: Append(T, L2)}
     }
   }
 }
diff --git a/src/examples/list_c_types.h b/src/examples/list_c_types.h
index c9b6d7a0..7caa03b3 100644
--- a/src/examples/list_c_types.h
+++ b/src/examples/list_c_types.h
@@ -1,17 +1,17 @@
-struct int_list {
+struct sllist {
   int head;
-  struct int_list* tail;
+  struct sllist* tail;
 };
 
-extern struct int_list *mallocIntList();
-/*@ spec mallocIntList();
+extern struct sllist *malloc__sllist();
+/*@ spec malloc__sllist();
     requires true;
-    ensures take u = Block<struct int_list>(return);
+    ensures take R = Block<struct sllist>(return);
 @*/
 
-extern void freeIntList (struct int_list *p);
-/*@ spec freeIntList(pointer p);
-    requires take u = Block<struct int_list>(p);
+extern void free__sllist (struct sllist *p);
+/*@ spec free__sllist(pointer p);
+    requires take P = Block<struct sllist>(p);
     ensures true;
 @*/
 
diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h
index d45e6537..14ef5da2 100644
--- a/src/examples/list_cn_types.h
+++ b/src/examples/list_cn_types.h
@@ -1,16 +1,16 @@
 /*@
-datatype seq {
-  Seq_Nil {},
-  Seq_Cons {i32 head, datatype seq tail}
+datatype List {
+  Nil {},
+  Cons {i32 Head, datatype List Tail}
 }
 
-predicate (datatype seq) IntList(pointer p) {
+predicate (datatype List) SLList(pointer p) {
   if (is_null(p)) {
-    return Seq_Nil{};
+    return Nil{};
   } else {
-    take H = Owned<struct int_list>(p);
-    take tl = IntList(H.tail);
-    return (Seq_Cons { head: H.head, tail: tl });
+    take H = Owned<struct sllist>(p);
+    take T = SLList(H.tail);
+    return (Cons { Head: H.head, Tail: T });
   }
 }
 @*/
diff --git a/src/examples/list_constructors.h b/src/examples/list_constructors.h
index 2108a861..178fd8f7 100644
--- a/src/examples/list_constructors.h
+++ b/src/examples/list_constructors.h
@@ -1,18 +1,18 @@
-struct int_list* IntList_nil()
-/*@ ensures take ret = IntList(return);
-            ret == Seq_Nil{};
+struct sllist* slnil()
+/*@ ensures take Ret = SLList(return);
+            Ret == Nil{};
  @*/
 {
   return 0;
 }
 
-struct int_list* IntList_cons(int h, struct int_list* t)
-/*@ requires take l = IntList(t);
-    ensures take ret = IntList(return);
-            ret == Seq_Cons{ head: h, tail: l};
+struct sllist* slcons(int h, struct sllist* t)
+/*@ requires take T = SLList(t);
+    ensures take Ret = SLList(return);
+            Ret == Cons{ Head: h, Tail: T};
  @*/
 {
-  struct int_list *p = mallocIntList();
+  struct sllist *p = malloc__sllist();
   p->head = h;
   p->tail = t;
   return p;
diff --git a/src/examples/list_copy.c b/src/examples/list_copy.c
index 4a1f8ef6..d45678da 100644
--- a/src/examples/list_copy.c
+++ b/src/examples/list_copy.c
@@ -1,17 +1,17 @@
 #include "list.h"
 
-struct int_list* IntList_copy (struct int_list *xs)
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            take L2 = IntList(return);
-            L1 == L1_;
-            L1 == L2;
+struct sllist* slcopy (struct sllist *l)
+/*@ requires take L = SLList(l);
+    ensures take L_ = SLList(l);
+            take Ret = SLList(return);
+            L == L_;
+            L == Ret;
 @*/
 {
-  if (xs == 0) {
-    return IntList_nil();
+  if (l == 0) {
+    return slnil();
   } else {
-    struct int_list *new_tail = IntList_copy(xs->tail);
-    return IntList_cons(xs->head, new_tail);
+    struct sllist *new_tail = slcopy(l->tail);
+    return slcons(l->head, new_tail);
   }
 }
diff --git a/src/examples/list_free.c b/src/examples/list_free.c
index f1441f4b..db3a6f06 100644
--- a/src/examples/list_free.c
+++ b/src/examples/list_free.c
@@ -1,14 +1,14 @@
 #include "list.h"
 
-void IntList_free_list(struct int_list* xs)
+void free__rec_sllist(struct sllist* l)
 // You fill in the rest...
 /* --BEGIN-- */
-/*@ requires take L1 = IntList(xs); @*/
+/*@ requires take L = SLList(l); @*/
 {
-  if (xs == 0) {
+  if (l == 0) {
   } else {
-    IntList_free_list(xs->tail);
-    freeIntList(xs);
+    free__rec_sllist(l->tail);
+    free__sllist(l);
   }
 }
 /* --END-- */
diff --git a/src/examples/list_hdtl.h b/src/examples/list_hdtl.h
index e92b51ed..e36738ff 100644
--- a/src/examples/list_hdtl.h
+++ b/src/examples/list_hdtl.h
@@ -1,22 +1,22 @@
 /*@
-function (i32) hd (datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
+function (i32) Hd (datatype List L) {
+  match L {
+    Nil {} => {
       0i32
     }
-    Seq_Cons {head : h, tail : _} => {
-      h
+    Cons {Head : H, Tail : _} => {
+      H
     }
   }
 }
 
-function (datatype seq) tl (datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
-      Seq_Nil {}
+function (datatype List) Tl (datatype List L) {
+  match L {
+    Nil {} => {
+      Nil{}
     }
-    Seq_Cons {head : _, tail : tail} => {
-      tail
+    Cons {Head : _, Tail : T} => {
+      T
     }
   }
 }
diff --git a/src/examples/list_length.c b/src/examples/list_length.c
index 047b2c30..832eb7ef 100644
--- a/src/examples/list_length.c
+++ b/src/examples/list_length.c
@@ -1,40 +1,38 @@
-/* list_length.c */
-
 #include "list.h"
 
 /* --BEGIN-- */
 /*@
-function [rec] (u32) length(datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
+function [rec] (u32) Length(datatype List L) {
+  match L {
+    Nil {} => {
       0u32
     }
-    Seq_Cons {head : h, tail : zs}  => {
-      1u32 + length(zs)
+    Cons {Head: H, Tail : T}  => {
+      1u32 + Length(T)
     }
   }
 }
 @*/
 
 /* --END-- */
-unsigned int IntList_length (struct int_list *xs)
+unsigned int length (struct sllist *l)
 /* --BEGIN-- */
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            L1 == L1_;
-            return == length(L1);
+/*@ requires take L = SLList(l);
+    ensures take L_post = SLList(l);
+            L == L_post;
+            return == Length(L);
 @*/
 /* --END-- */
 {
-  if (xs == 0) {
+  if (l == 0) {
 /* --BEGIN-- */
-    /*@ unfold length(L1); @*/
+    /*@ unfold Length(L); @*/
 /* --END-- */
     return 0;
   } else {
 /* --BEGIN-- */
-    /*@ unfold length(L1); @*/
+    /*@ unfold Length(L); @*/
 /* --END-- */
-    return 1 + IntList_length (xs->tail);
+    return 1 + length(l->tail);
   }
 }
diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c
index 653ad0af..584e5988 100644
--- a/src/examples/list_rev.c
+++ b/src/examples/list_rev.c
@@ -3,30 +3,30 @@
 #include "list_rev.h"
 #include "list_rev_lemmas.h"
 
-struct int_list* IntList_rev_aux(struct int_list* xs, struct int_list* ys)
-/*@ requires take L1 = IntList(xs); @*/
-/*@ requires take L2 = IntList(ys); @*/
-/*@ ensures take R = IntList(return); @*/
-/*@ ensures R == append(rev(L2), L1); @*/
+struct sllist* rev_aux(struct sllist* l1, struct sllist* l2)
+/*@ requires take L1 = SLList(l1); @*/
+/*@ requires take L2 = SLList(l2); @*/
+/*@ ensures take R = SLList(return); @*/
+/*@ ensures R == Append(RevList(L2), L1); @*/
 {
-  if (ys == 0) {
-    /*@ unfold rev(L2); @*/
-    /*@ unfold append(Seq_Nil {},L1); @*/
-    return xs;
+  if (l2 == 0) {
+    /*@ unfold RevList(L2); @*/
+    /*@ unfold Append(Nil{}, L1); @*/
+    return l1;
   } else {
-    /*@ unfold rev(L2); @*/
-    /*@ apply append_cons_r(rev(tl(L2)), hd(L2), L1); @*/
-    struct int_list *tmp = ys->tail;
-    ys->tail = xs;
-    return IntList_rev_aux(ys, tmp);
+    /*@ unfold RevList(L2); @*/
+    /*@ apply Append_Cons_RList(RevList(Tl(L2)), Hd(L2), L1); @*/
+    struct sllist *tmp = l2->tail;
+    l2->tail = l1;
+    return rev_aux(l2, tmp);
   }
 }
 
-struct int_list* IntList_rev(struct int_list* xs)
-/*@ requires take L1 = IntList(xs); @*/
-/*@ ensures take L1_rev = IntList(return); @*/
-/*@ ensures L1_rev == rev(L1); @*/
+struct sllist* rev(struct sllist* l1)
+/*@ requires take L1 = SLList(l1); @*/
+/*@ ensures take L1_Rev = SLList(return); @*/
+/*@ ensures L1_Rev == RevList(L1); @*/
 {
-  /*@ apply append_nil_r(rev(L1)); @*/
-  return IntList_rev_aux (0, xs);
+  /*@ apply Append_Nil_RList(RevList(L1)); @*/
+  return rev_aux (0, l1);
 }
diff --git a/src/examples/list_rev.h b/src/examples/list_rev.h
index 7260f3eb..eeda4df0 100644
--- a/src/examples/list_rev.h
+++ b/src/examples/list_rev.h
@@ -1,13 +1,13 @@
 #include "list_snoc.h"
 
 /*@
-function [rec] (datatype seq) rev(datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
-      Seq_Nil {}
+function [rec] (datatype List) RevList(datatype List L) {
+  match L {
+    Nil {} => {
+      Nil {}
     }
-    Seq_Cons {head : h, tail : zs}  => {
-      snoc (rev(zs), h)
+    Cons {Head : H, Tail : T}  => {
+      Snoc (RevList(T), H)
     }
   }
 }
diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c
index 7cb4eaa5..6d3ec343 100644
--- a/src/examples/list_rev_alt.c
+++ b/src/examples/list_rev_alt.c
@@ -3,31 +3,31 @@
 #include "list_rev.h"
 #include "list_rev_lemmas.h"
 
-struct int_list* IntList_rev_loop(struct int_list *xs)
-/*@ requires take L = IntList(xs);
-    ensures  take L_ = IntList(return);
-             L_ == rev(L);
+struct sllist* rev_loop(struct sllist *l)
+/*@ requires take L = SLList(l);
+    ensures  take L_post = SLList(return);
+             L_post == RevList(L);
 @*/
 {
-  struct int_list *last = 0;
-  struct int_list *cur = xs;
-  /*@ apply append_nil_r(rev(L)); @*/
+  struct sllist *last = 0;
+  struct sllist *cur = l;
+  /*@ apply Append_Nil_RList(RevList(L)); @*/
   while(1)
-  /*@ inv take L1 = IntList(last);
-          take L2 = IntList(cur);
-          append(rev(L2), L1) == rev(L);
+  /*@ inv take Last = SLList(last);
+          take Cur = SLList(cur);
+          Append(RevList(Cur), Last) == RevList(L);
   @*/
   {
     if (cur == 0) {
-      /*@ unfold rev(Seq_Nil {}); @*/
-      /*@ unfold append(Seq_Nil {}, L1); @*/
+      /*@ unfold RevList(Nil{}); @*/
+      /*@ unfold Append(Nil{}, Last); @*/
       return last;
     }
-    struct int_list *tmp = cur->tail;
+    struct sllist *tmp = cur->tail;
     cur->tail = last;
     last = cur;
     cur = tmp;
-    /*@ unfold rev(L2); @*/
-    /*@ apply append_cons_r (rev (tl(L2)), hd(L2), L1); @*/
+    /*@ unfold RevList(Cur); @*/
+    /*@ apply Append_Cons_RList(RevList(Tl(Cur)), Hd(Cur), Last); @*/
   }
 }
diff --git a/src/examples/list_rev_lemmas.h b/src/examples/list_rev_lemmas.h
index 28f21937..8e6dd044 100644
--- a/src/examples/list_rev_lemmas.h
+++ b/src/examples/list_rev_lemmas.h
@@ -1,10 +1,10 @@
 /*@
-lemma append_nil_r (datatype seq l1)
+lemma Append_Nil_RList (datatype List L1)
   requires true;
-  ensures append(l1, Seq_Nil {}) == l1;
+  ensures Append(L1, Nil{}) == L1;
 
-lemma append_cons_r (datatype seq l1, i32 x, datatype seq l2)
+lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2)
   requires true;
-  ensures append(l1, Seq_Cons {head: x, tail: l2})
-          == append(snoc(l1, x), l2);
+  ensures Append(L1, Cons {Head: X, Tail: L2})
+          == Append(Snoc(L1, X), L2);
 @*/
diff --git a/src/examples/list_snoc.h b/src/examples/list_snoc.h
index 52cbdcb4..97a27f77 100644
--- a/src/examples/list_snoc.h
+++ b/src/examples/list_snoc.h
@@ -1,11 +1,11 @@
 /*@
-function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
-  match xs {
-    Seq_Nil {} => {
-      Seq_Cons {head: y, tail: Seq_Nil{}}
+function [rec] (datatype List) Snoc(datatype List Xs, i32 Y) {
+  match Xs {
+    Nil {} => {
+      Cons {Head: Y, Tail: Nil{}}
     }
-    Seq_Cons {head: x, tail: zs}  => {
-      Seq_Cons{head: x, tail: snoc (zs, y)}
+    Cons {Head: X, Tail: Zs}  => {
+      Cons{Head: X, Tail: Snoc (Zs, Y)}
     }
   }
 }
diff --git a/src/examples/liste_rev_lemmas.h b/src/examples/liste_rev_lemmas.h
index c4554e40..8bc6f870 100644
--- a/src/examples/liste_rev_lemmas.h
+++ b/src/examples/liste_rev_lemmas.h
@@ -1,10 +1,10 @@
 /*@
-lemma append_nil_r (datatype seq l1)
+lemma Append_nil_r (datatype List l1)
   requires true
-  ensures append(l1, Seq_Nil {}) == l1
+  ensures Append(l1, Nil {}) == l1
 
-lemma append_cons_r (datatype seq l1, i32 x, datatype seq l2)
+lemma Append_cons_r (datatype List l1, i32 x, datatype List l2)
   requires true
-  ensures append(l1, Seq_Cons {head: x, tail: l2})
-          == append(snoc(l1, x), l2)
+  ensures Append(l1, Cons {Head: x, Tail: l2})
+          == Append(snoc(l1, x), l2)
 @*/
diff --git a/src/examples/malloc.h b/src/examples/malloc.h
index 7182d1a2..fe2c2fc2 100644
--- a/src/examples/malloc.h
+++ b/src/examples/malloc.h
@@ -1,13 +1,12 @@
 extern int *mallocInt ();
 /*@ spec mallocInt();
     requires true;
-    ensures take v = Block<int>(return);
+    ensures take R = Block<int>(return);
 @*/
 
-
 extern unsigned int *mallocUnsignedInt ();
 /*@ spec mallocUnsignedInt();
     requires true;
-    ensures take v = Block<unsigned int>(return);
+    ensures take R = Block<unsigned int>(return);
 @*/
 
diff --git a/src/examples/mergesort.c b/src/examples/mergesort.c
index 5c6c13bd..5076166d 100644
--- a/src/examples/mergesort.c
+++ b/src/examples/mergesort.c
@@ -1,44 +1,45 @@
 #include "list.h"
 
 /*@
-function [rec] ({datatype seq fst, datatype seq snd}) split(datatype seq xs)
+function [rec] ({datatype List fst, datatype List snd}) 
+                 split (datatype List xs)
 {
   match xs {
-    Seq_Nil {} => {
-      {fst: Seq_Nil{}, snd: Seq_Nil{}}
+    Nil {} => {
+      {fst: Nil{}, snd: Nil{}}
     }
-    Seq_Cons {head: h1, tail: Seq_Nil{}} => {
-      {fst: Seq_Nil{}, snd: xs}
+    Cons {Head: h1, Tail: Nil{}} => {
+      {fst: Nil{}, snd: xs}
     }
-    Seq_Cons {head: h1, tail: Seq_Cons {head : h2, tail : tl2 }} => {
+    Cons {Head: h1, Tail: Cons {Head : h2, Tail : tl2 }} => {
       let P = split(tl2);
-      {fst: Seq_Cons { head: h1, tail: P.fst},
-       snd: Seq_Cons { head: h2, tail: P.snd}}
+      {fst: Cons { Head: h1, Tail: P.fst},
+       snd: Cons { Head: h2, Tail: P.snd}}
     }
   }
 }
 
-function [rec] (datatype seq) merge(datatype seq xs, datatype seq ys) {
+function [rec] (datatype List) merge(datatype List xs, datatype List ys) {
   match xs {
-      Seq_Nil {} => { ys }
-      Seq_Cons {head: x, tail: xs1} => {
+      Nil {} => { ys }
+      Cons {Head: x, Tail: xs1} => {
         match ys {
-          Seq_Nil {} => { xs }
-          Seq_Cons{ head: y, tail: ys1} => {
+          Nil {} => { xs }
+          Cons{ Head: y, Tail: ys1} => {
             (x < y) ?
-              (Seq_Cons{ head: x, tail: merge(xs1, ys) })
-            : (Seq_Cons{ head: y, tail: merge(xs, ys1) })
+              (Cons{ Head: x, Tail: merge(xs1, ys) })
+            : (Cons{ Head: y, Tail: merge(xs, ys1) })
           }
         }
       }
   }
 }
 
-function [rec] (datatype seq) mergesort(datatype seq xs) {
+function [rec] (datatype List) mergesort(datatype List xs) {
   match xs {
-      Seq_Nil{} => { xs }
-      Seq_Cons{head: x, tail: Seq_Nil{}} => { xs }
-      Seq_Cons{head: x, tail: Seq_Cons{head: y, tail: zs}} => {
+      Nil{} => { xs }
+      Cons{Head: x, Tail: Nil{}} => { xs }
+      Cons{Head: x, Tail: Cons{Head: y, Tail: zs}} => {
         let P = split(xs);
         let L1 = mergesort(P.fst);
         let L2 = mergesort(P.snd);
@@ -48,42 +49,42 @@ function [rec] (datatype seq) mergesort(datatype seq xs) {
 }
 @*/
 
-struct int_list_pair {
-  struct int_list* fst;
-  struct int_list* snd;
+struct sllist_pair {
+  struct sllist* fst;
+  struct sllist* snd;
 };
 
-struct int_list_pair split(struct int_list *xs)
-/*@ requires take Xs = IntList(xs); @*/
-/*@ ensures take Ys = IntList(return.fst); @*/
-/*@ ensures take Zs = IntList(return.snd); @*/
+struct sllist_pair split(struct sllist *xs)
+/*@ requires take Xs = SLList(xs); @*/
+/*@ ensures take Ys = SLList(return.fst); @*/
+/*@ ensures take Zs = SLList(return.snd); @*/
 /*@ ensures {fst: Ys, snd: Zs} == split(Xs); @*/
 {
   if (xs == 0) {
     /*@ unfold split(Xs); @*/
-    struct int_list_pair r = {.fst = 0, .snd = 0};
+    struct sllist_pair r = {.fst = 0, .snd = 0};
     return r;
   } else {
-    struct int_list *cdr = xs -> tail;
+    struct sllist *cdr = xs -> tail;
     if (cdr == 0) {
       /*@ unfold split(Xs); @*/
-      struct int_list_pair r = {.fst = 0, .snd = xs};
+      struct sllist_pair r = {.fst = 0, .snd = xs};
       return r;
     } else {
       /*@ unfold split(Xs); @*/
-      struct int_list_pair p = split(cdr->tail);
+      struct sllist_pair p = split(cdr->tail);
       xs->tail = p.fst;
       cdr->tail = p.snd;
-      struct int_list_pair r = {.fst = xs, .snd = cdr};
+      struct sllist_pair r = {.fst = xs, .snd = cdr};
       return r;
     }
   }
 }
 
-struct int_list* merge(struct int_list *xs, struct int_list *ys)
-/*@ requires take Xs = IntList(xs); @*/
-/*@ requires take Ys = IntList(ys); @*/
-/*@ ensures take Zs = IntList(return); @*/
+struct sllist* merge(struct sllist *xs, struct sllist *ys)
+/*@ requires take Xs = SLList(xs); @*/
+/*@ requires take Ys = SLList(ys); @*/
+/*@ ensures take Zs = SLList(return); @*/
 /*@ ensures Zs == merge(Xs, Ys); @*/
 {
   if (xs == 0) {
@@ -97,11 +98,11 @@ struct int_list* merge(struct int_list *xs, struct int_list *ys)
     } else {
       /*@ unfold merge(Xs, Ys); @*/
       if (xs->head < ys->head) {
-        struct int_list *zs = merge(xs->tail, ys);
+        struct sllist *zs = merge(xs->tail, ys);
         xs->tail = zs;
         return xs;
       } else {
-        struct int_list *zs = merge(xs, ys->tail);
+        struct sllist *zs = merge(xs, ys->tail);
         ys->tail = zs;
         return ys;
       }
@@ -109,22 +110,22 @@ struct int_list* merge(struct int_list *xs, struct int_list *ys)
   }
 }
 
-struct int_list* mergesort(struct int_list *xs)
-/*@ requires take Xs = IntList(xs); @*/
-/*@ ensures take Ys = IntList(return); @*/
+struct sllist* mergesort(struct sllist *xs)
+/*@ requires take Xs = SLList(xs); @*/
+/*@ ensures take Ys = SLList(return); @*/
 /*@ ensures Ys == mergesort(Xs); @*/
 {
   if (xs == 0) {
     /*@ unfold mergesort(Xs); @*/
     return xs;
   } else {
-    struct int_list *tail = xs->tail;
+    struct sllist *tail = xs->tail;
     if (tail == 0) {
       /*@ unfold mergesort(Xs); @*/
       return xs;
     } else {
       /*@ unfold mergesort(Xs); @*/
-      struct int_list_pair p = split(xs);
+      struct sllist_pair p = split(xs);
       p.fst = mergesort(p.fst);
       p.snd = mergesort(p.snd);
       return merge(p.fst, p.snd);
diff --git a/src/examples/queue_allocation.h b/src/examples/queue_allocation.h
index 6415601f..430c144a 100644
--- a/src/examples/queue_allocation.h
+++ b/src/examples/queue_allocation.h
@@ -1,23 +1,23 @@
 extern struct int_queue *mallocIntQueue();
 /*@ spec mallocIntQueue();
     requires true;
-    ensures take u = Block<struct int_queue>(return);
+    ensures take R = Block<struct int_queue>(return);
 @*/ 
 
 extern void freeIntQueue (struct int_queue *p);
 /*@ spec freeIntQueue(pointer p);
-    requires take u = Block<struct int_queue>(p);
+    requires take P = Block<struct int_queue>(p);
     ensures true;
 @*/
 
 extern struct int_queueCell *mallocIntQueueCell();
 /*@ spec mallocIntQueueCell();
     requires true;
-    ensures take u = Block<struct int_queueCell>(return);
+    ensures take R = Block<struct int_queueCell>(return);
 @*/ 
 
 extern void freeIntQueueCell (struct int_queueCell *p);
 /*@ spec freeIntQueueCell(pointer p);
-    requires take u = Block<struct int_queueCell>(p);
+    requires take P = Block<struct int_queueCell>(p);
     ensures true;
 @*/
diff --git a/src/examples/queue_cn_types_1.h b/src/examples/queue_cn_types_1.h
index 705eff65..0066a60a 100644
--- a/src/examples/queue_cn_types_1.h
+++ b/src/examples/queue_cn_types_1.h
@@ -1,5 +1,5 @@
 /*@
-predicate (datatype seq) IntQueuePtr (pointer q) {
+predicate (datatype List) IntQueuePtr (pointer q) {
   take Q = Owned<struct int_queue>(q);
   assert (   (is_null(Q.front)  && is_null(Q.back)) 
           || (!is_null(Q.front) && !is_null(Q.back)));
diff --git a/src/examples/queue_cn_types_2.h b/src/examples/queue_cn_types_2.h
index d8e724f3..5d1f825c 100644
--- a/src/examples/queue_cn_types_2.h
+++ b/src/examples/queue_cn_types_2.h
@@ -1,12 +1,12 @@
 /*@
-predicate (datatype seq) IntQueueFB (pointer front, pointer back) {
+predicate (datatype List) IntQueueFB (pointer front, pointer back) {
   if (is_null(front)) {
-    return Seq_Nil{};
+    return Nil{};
   } else {
     take B = Owned<struct int_queueCell>(back);
     assert (is_null(B.next));
     take L = IntQueueAux (front, back);
-    return snoc(L, B.first);
+    return Snoc(L, B.first);
   }
 }
 @*/
diff --git a/src/examples/queue_cn_types_3.h b/src/examples/queue_cn_types_3.h
index 99f22eb0..721930a3 100644
--- a/src/examples/queue_cn_types_3.h
+++ b/src/examples/queue_cn_types_3.h
@@ -1,12 +1,12 @@
 /*@
-predicate (datatype seq) IntQueueAux (pointer f, pointer b) {
+predicate (datatype List) IntQueueAux (pointer f, pointer b) {
   if (ptr_eq(f,b)) {
-    return Seq_Nil{};
+    return Nil{};
   } else {
     take F = Owned<struct int_queueCell>(f);
     assert (!is_null(F.next));  
     take B = IntQueueAux(F.next, b);
-    return Seq_Cons{head: F.first, tail: B};
+    return Cons{Head: F.first, Tail: B};
   }
 }
 @*/
diff --git a/src/examples/queue_empty.c b/src/examples/queue_empty.c
index d2a8f3c7..27c0b921 100644
--- a/src/examples/queue_empty.c
+++ b/src/examples/queue_empty.c
@@ -3,7 +3,7 @@
 struct int_queue* IntQueue_empty ()
 /* --BEGIN-- */
 /*@ ensures take ret = IntQueuePtr(return);
-            ret == Seq_Nil{};
+            ret == Nil{};
 @*/
 /* --END-- */
 {
diff --git a/src/examples/queue_pop.c b/src/examples/queue_pop.c
index d1053c25..d7f989a8 100644
--- a/src/examples/queue_pop.c
+++ b/src/examples/queue_pop.c
@@ -2,11 +2,11 @@
 #include "queue_pop_lemma.h"
 
 int IntQueue_pop (struct int_queue *q)
-/*@ requires take before = IntQueuePtr(q);
-             before != Seq_Nil{};
-    ensures take after = IntQueuePtr(q);
-            after == tl(before);
-            return == hd(before);
+/*@ requires take Q = IntQueuePtr(q);
+             Q != Nil{};
+    ensures take Q_post = IntQueuePtr(q);
+            Q_post == Tl(Q);
+            return == Hd(Q);
 @*/
 {
   /*@ split_case is_null(q->front); @*/
@@ -16,7 +16,7 @@ int IntQueue_pop (struct int_queue *q)
     freeIntQueueCell(h);
     q->front = 0;
     q->back = 0;
-    /*@ unfold snoc(Seq_Nil{}, x); @*/
+    /*@ unfold Snoc(Nil{}, x); @*/
     return x;
   } else {
     int x = h->first;
diff --git a/src/examples/queue_pop_lemma.h b/src/examples/queue_pop_lemma.h
index 80d2ab90..f2f46f40 100644
--- a/src/examples/queue_pop_lemma.h
+++ b/src/examples/queue_pop_lemma.h
@@ -7,7 +7,7 @@ lemma snoc_facts (pointer front, pointer back, i32 x)
       take NewQ = IntQueueAux(front, back);
       take NewB = Owned<struct int_queueCell>(back);
       Q == NewQ; B == NewB;
-      let L = snoc (Seq_Cons{head: x, tail: Q}, B.first);
-      hd(L) == x;
-      tl(L) == snoc (Q, B.first);
+      let L = Snoc (Cons{Head: x, Tail: Q}, B.first);
+      Hd(L) == x;
+      Tl(L) == Snoc (Q, B.first);
 @*/
diff --git a/src/examples/queue_pop_lemma_stages.c b/src/examples/queue_pop_lemma_stages.c
index 66043b8d..7ef87259 100644
--- a/src/examples/queue_pop_lemma_stages.c
+++ b/src/examples/queue_pop_lemma_stages.c
@@ -5,22 +5,22 @@
 
 /*@
 
-predicate (datatype seq) Pre(pointer front, pointer back, i32 popped, datatype seq before) {
+predicate (datatype List) Pre(pointer front, pointer back, i32 popped, datatype List before) {
   if (is_null(front)) {
-    let after = Seq_Nil{};
-    assert (before == snoc(Seq_Nil{}, popped));
+    let after = Nil{};
+    assert (before == Snoc(Nil{}, popped));
     return after;
   } else {
     take B = Owned<struct int_queueCell>(back);
     assert (is_null(B.next));
     take L = IntQueueAux (front, back);
-    assert (before == snoc(Seq_Cons {head: popped, tail: L}, B.first));
-    let after = snoc(L, B.first);
+    assert (before == Snoc(Cons {Head: popped, Tail: L}, B.first));
+    let after = Snoc(L, B.first);
     return after;
   }
 }
 
-lemma lemma1(pointer front, pointer back, i32 popped, datatype seq before)
+lemma lemma1(pointer front, pointer back, i32 popped, datatype List before)
 requires
     take Q = Pre(front, back, popped, before);
 ensures
@@ -32,26 +32,26 @@ ensures
 
 /*@
 
-predicate (datatype seq) Post(pointer front, pointer back, i32 popped, datatype seq before) {
+predicate (datatype List) Post(pointer front, pointer back, i32 popped, datatype List before) {
   if (is_null(front)) {
-    assert (before == snoc(Seq_Nil{}, popped));
-    let after = Seq_Nil{};
-    assert (after == tl(before));
-    assert (popped == hd(before));
+    assert (before == Snoc(Nil{}, popped));
+    let after = Nil{};
+    assert (after == Tl(before));
+    assert (popped == Hd(before));
     return after;
   } else {
     take B = Owned<struct int_queueCell>(back);
     assert (is_null(B.next));
     take L = IntQueueAux (front, back);
-    assert (before == snoc(Seq_Cons {head: popped, tail: L}, B.first));
-    let after = snoc(L, B.first);
-    assert (after == tl(before));
-    assert (popped == hd(before));
+    assert (before == Snoc(Cons {Head: popped, Tail: L}, B.first));
+    let after = Snoc(L, B.first);
+    assert (after == Tl(before));
+    assert (popped == Hd(before));
     return after;
   }
 }
 
-lemma lemma2(pointer front, pointer back, i32 popped, datatype seq before)
+lemma lemma2(pointer front, pointer back, i32 popped, datatype List before)
 requires
     take Q = Pre(front, back, popped, before);
 ensures
@@ -65,28 +65,28 @@ ensures
 
 /*@
 
-type_synonym result = { datatype seq after, datatype seq before }
+type_synonym result = { datatype List after, datatype List before }
 
 predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) {
   if (is_null(front)) {
-    return { after: Seq_Nil{}, before: snoc(Seq_Nil{}, popped) };
+    return { after: Nil{}, before: Snoc(Nil{}, popped) };
   } else {
     take B = Owned<struct int_queueCell>(back);
     assert (is_null(B.next));
     take L = IntQueueAux (front, back);
-    return { after: snoc(L, B.first), before: snoc(Seq_Cons {head: popped, tail: L}, B.first) };
+    return { after: Snoc(L, B.first), before: Snoc(Cons {Head: popped, Tail: L}, B.first) };
   }
 }
 
-lemma lemma3(pointer front, pointer back, i32 popped, datatype seq before)
+lemma lemma3(pointer front, pointer back, i32 popped, datatype List before)
 requires
     take Q = Queue_pop_lemma(front, back, popped);
     before == Q.before;
 ensures
     take NewQ = Queue_pop_lemma(front, back, popped);
     Q == NewQ;
-    Q.after == tl(Q.before);
-    popped == hd(Q.before);
+    Q.after == Tl(Q.before);
+    popped == Hd(Q.before);
 @*/
 
 // Step 4 (optional): Remove the sanity checking from the pre-condition.
@@ -99,7 +99,7 @@ requires
 ensures
     take NewQ = Queue_pop_lemma(front, back, popped);
     Q == NewQ;
-    Q.after == tl(Q.before);
-    popped == hd(Q.before);
+    Q.after == Tl(Q.before);
+    popped == Hd(Q.before);
 
 @*/
diff --git a/src/examples/queue_pop_unified.c b/src/examples/queue_pop_unified.c
index da0b8018..f15f0136 100644
--- a/src/examples/queue_pop_unified.c
+++ b/src/examples/queue_pop_unified.c
@@ -1,16 +1,16 @@
 #include "queue_headers.h"
 
 /*@
-type_synonym result = { datatype seq after, datatype seq before }
+type_synonym result = { datatype List after, datatype List before }
 
 predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) {
   if (is_null(front)) {
-    return { after: Seq_Nil{}, before: snoc(Seq_Nil{}, popped) };
+    return { after: Nil{}, before: Snoc(Nil{}, popped) };
   } else {
     take B = Owned<struct int_queueCell>(back);
     assert (is_null(B.next));
     take L = IntQueueAux (front, back);
-    return { after: snoc(L, B.first), before: snoc(Seq_Cons {head: popped, tail: L}, B.first) };
+    return { after: Snoc(L, B.first), before: Snoc(Cons {Head: popped, Tail: L}, B.first) };
   }
 }
 @*/
@@ -24,12 +24,12 @@ ensures
     take NewQ = IntQueueAux(front, back);
     take NewB = Owned<struct int_queueCell>(back);
     Q == NewQ; B == NewB;
-    let L = snoc (Seq_Cons{head: x, tail: Q}, B.first);
-    hd(L) == x;
-    tl(L) == snoc (Q, B.first);
+    let L = Snoc (Cons{Head: x, Tail: Q}, B.first);
+    Hd(L) == x;
+    Tl(L) == Snoc (Q, B.first);
 @*/
 {
-    /*@ unfold snoc (Seq_Cons{head: x, tail: Q}, B.first); @*/
+    /*@ unfold Snoc (Cons{Head: x, Tail: Q}, B.first); @*/
 }
 
 void snoc_fact_unified(struct int_queueCell *front, struct int_queueCell *back, int x)
@@ -39,12 +39,12 @@ requires
 ensures
       take NewAB = Queue_pop_lemma(front, back, x);
       AB == NewAB;
-      AB.after == tl(AB.before);
-      x == hd(AB.before);
+      AB.after == Tl(AB.before);
+      x == Hd(AB.before);
 @*/
 {
     if (!front) {
-        /*@ unfold snoc(Seq_Nil{}, x); @*/
+        /*@ unfold Snoc(Nil{}, x); @*/
     } else {
         snoc_fact(front, back, x);
     }
@@ -52,10 +52,10 @@ ensures
 
 int IntQueue_pop (struct int_queue *q)
 /*@ requires take before = IntQueuePtr(q);
-             before != Seq_Nil{};
+             before != Nil{};
     ensures take after = IntQueuePtr(q);
-            after == tl(before);
-            return == hd(before);
+            after == Tl(before);
+            return == Hd(before);
 @*/
 {
   /*@ split_case is_null(q->front); @*/
diff --git a/src/examples/queue_push.c b/src/examples/queue_push.c
index e22dd152..ede31857 100644
--- a/src/examples/queue_push.c
+++ b/src/examples/queue_push.c
@@ -2,9 +2,9 @@
 #include "queue_push_lemma.h" 
 
 void IntQueue_push (int x, struct int_queue *q)
-/*@ requires take before = IntQueuePtr(q);
-    ensures take after = IntQueuePtr(q);
-            after == snoc (before, x);
+/*@ requires take Q = IntQueuePtr(q);
+    ensures take Q_post = IntQueuePtr(q);
+            Q_post == Snoc (Q, x);
 @*/
 {
   struct int_queueCell *c = mallocIntQueueCell();
diff --git a/src/examples/queue_push_induction.c b/src/examples/queue_push_induction.c
index 9d0f897a..d607b896 100644
--- a/src/examples/queue_push_induction.c
+++ b/src/examples/queue_push_induction.c
@@ -12,16 +12,16 @@ void push_induction(struct int_queueCell* front
   ensures
       take NewQ = IntQueueAux(front, last);
       take Last2 = Owned(last);
-      NewQ == snoc(Q, Second_last.first);
+      NewQ == Snoc(Q, Second_last.first);
       Last == Last2;
 @*/
 {
     if (front == second_last) {
-        /*@ unfold snoc(Q, Second_last.first); @*/
+        /*@ unfold Snoc(Q, Second_last.first); @*/
         return;
     } else {
         push_induction(front->next, second_last, last);
-        /*@ unfold snoc(Q, Second_last.first); @*/
+        /*@ unfold Snoc(Q, Second_last.first); @*/
         return;
     }
 }
@@ -29,7 +29,7 @@ void push_induction(struct int_queueCell* front
 void IntQueue_push (int x, struct int_queue *q)
 /*@ requires take before = IntQueuePtr(q);
     ensures take after = IntQueuePtr(q);
-            after == snoc (before, x);
+            after == Snoc (before, x);
 @*/
 {
   struct int_queueCell *c = mallocIntQueueCell();
diff --git a/src/examples/queue_push_lemma.h b/src/examples/queue_push_lemma.h
index d3052dc2..740d98c0 100644
--- a/src/examples/queue_push_lemma.h
+++ b/src/examples/queue_push_lemma.h
@@ -4,6 +4,6 @@ lemma push_lemma (pointer front, pointer p)
       take Q = IntQueueAux(front, p);
       take P = Owned<struct int_queueCell>(p);
   ensures
-      take NewQ = IntQueueAux(front, P.next);
-      NewQ == snoc(Q, P.first);
+      take Q_post = IntQueueAux(front, P.next);
+      NewQ == Snoc(Q, P.first);
 @*/
diff --git a/src/examples/read.c b/src/examples/read.c
index 5a09f6dd..04892f56 100644
--- a/src/examples/read.c
+++ b/src/examples/read.c
@@ -1,7 +1,7 @@
 int read (int *p)
 /* --BEGIN-- */
-/*@ requires take v1 = Owned<int>(p);
-    ensures take v2 = Owned<int>(p);
+/*@ requires take P = Owned<int>(p);
+    ensures take P_post = Owned<int>(p);
 @*/
 /* --END-- */
 {
diff --git a/src/examples/read2.c b/src/examples/read2.c
index d7fb90a7..94ca64ea 100644
--- a/src/examples/read2.c
+++ b/src/examples/read2.c
@@ -1,11 +1,9 @@
 int read (int *p)
-/* --BEGIN-- */
-/*@ requires take v1 = Owned<int>(p);
-    ensures take v2 = Owned<int>(p);
-            return == v1;
-            v1 == v2;
+/*@ requires take P = Owned<int>(p);
+    ensures take P_post = Owned<int>(p);
+            return == P;
+            P_post == P;
 @*/
-/* --END-- */
 {
   return *p;
 }
diff --git a/src/examples/ref.h b/src/examples/ref.h
index cbd68d5f..bbb83fa0 100644
--- a/src/examples/ref.h
+++ b/src/examples/ref.h
@@ -1,15 +1,14 @@
 extern unsigned int *refUnsignedInt (unsigned int v);
 /*@ spec refUnsignedInt(u32 v);
     requires true;
-    ensures take vr = Owned(return);
-            vr == v;
+    ensures take R = Owned(return);
+            R == v;
 @*/
 
-
 extern int *refInt (int v);
 /*@ spec refInt(i32 v);
     requires true;
-    ensures take vr = Owned(return);
-            vr == v;
+    ensures take R = Owned(return);
+            R == v;
 @*/
 
diff --git a/src/examples/slf0_basic_incr.c b/src/examples/slf0_basic_incr.c
index f954c842..51aa8f43 100644
--- a/src/examples/slf0_basic_incr.c
+++ b/src/examples/slf0_basic_incr.c
@@ -1,10 +1,8 @@
 void incr (unsigned int *p)
-/* --BEGIN-- */
 /*@ requires take n1 = Owned<unsigned int>(p);
     ensures take n2 = Owned<unsigned int>(p);
             n2 == n1 + 1u32;
 @*/
-/* --END-- */
 {
   unsigned int n = *p;
   unsigned int m = n+1;
diff --git a/src/examples/slf0_basic_incr.signed.broken.c b/src/examples/slf0_basic_incr.signed.broken.c
index a4959035..3fbd627d 100644
--- a/src/examples/slf0_basic_incr.signed.broken.c
+++ b/src/examples/slf0_basic_incr.signed.broken.c
@@ -1,6 +1,6 @@
 void incr (int *p)
-/*@ requires take u = Block<int>(p); 
-    ensures take v = Owned<int>(p); 
+/*@ requires take P = Block<int>(p); 
+    ensures take P_post = Owned<int>(p); 
 @*/
 {
   *p = *p+1;
diff --git a/src/examples/slf0_basic_incr.signed.c b/src/examples/slf0_basic_incr.signed.c
index ae0656d5..2986c617 100644
--- a/src/examples/slf0_basic_incr.signed.c
+++ b/src/examples/slf0_basic_incr.signed.c
@@ -1,11 +1,9 @@
 void incr (int *p)
-/* --BEGIN-- */
-/*@ requires take v1 = Owned<int>(p);
-             ((i64) v1) + 1i64 <= (i64)MAXi32();
-    ensures take v2 = Owned<int>(p);
-            v2 == v1+1i32;
+/*@ requires take P = Owned<int>(p);
+             ((i64) P) + 1i64 <= (i64) MAXi32();
+    ensures take P_post = Owned<int>(p);
+            P_post == P + 1i32;
 @*/
-/* --END-- */
 {
   *p = *p+1;
 }
diff --git a/src/examples/slf17_get_and_free.c b/src/examples/slf17_get_and_free.c
index 8c6e59aa..a2238315 100644
--- a/src/examples/slf17_get_and_free.c
+++ b/src/examples/slf17_get_and_free.c
@@ -1,8 +1,9 @@
 #include "free.h"
 
 unsigned int get_and_free (unsigned int *p)
-/*@ requires take v1_ = Owned(p);
-    ensures return == v1_; @*/
+/*@ requires take P = Owned(p);
+    ensures return == P; 
+@*/
 {
   unsigned int v = *p;
   freeUnsignedInt (p);
diff --git a/src/examples/slf1_basic_example_let.signed.c b/src/examples/slf1_basic_example_let.signed.c
index c3102646..44064ebd 100644
--- a/src/examples/slf1_basic_example_let.signed.c
+++ b/src/examples/slf1_basic_example_let.signed.c
@@ -1,8 +1,8 @@
 int doubled (int n)
 /* --BEGIN-- */
-/*@ requires let n_ = (i64) n;
-             (i64)MINi32() <= n_ - 1i64; n_ + 1i64 <= (i64)MAXi32();
-             (i64)MINi32() <= n_ + n_; n_ + n_ <= (i64)MAXi32();
+/*@ requires let N = (i64) n;
+             (i64)MINi32() <= N - 1i64; N + 1i64 <= (i64)MAXi32();
+             (i64)MINi32() <= N + N; N + N <= (i64)MAXi32();
     ensures return == n * 2i32;
 @*/
 /* --END-- */
diff --git a/src/examples/slf2_basic_quadruple.signed.c b/src/examples/slf2_basic_quadruple.signed.c
index 23a1d495..92e71f5d 100644
--- a/src/examples/slf2_basic_quadruple.signed.c
+++ b/src/examples/slf2_basic_quadruple.signed.c
@@ -1,7 +1,7 @@
 int quadruple (int n)
 /* --BEGIN-- */
-/*@ requires let n_ = (i64) n;
-             (i64)MINi32() <= n_ * 4i64; n_ * 4i64 <= (i64)MAXi32();
+/*@ requires let N = (i64) n;
+             (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32();
     ensures return == 4i32 * n;
  @*/
 /* --END-- */
diff --git a/src/examples/slf3_basic_inplace_double.c b/src/examples/slf3_basic_inplace_double.c
index 065a96f5..ca7cddde 100644
--- a/src/examples/slf3_basic_inplace_double.c
+++ b/src/examples/slf3_basic_inplace_double.c
@@ -1,10 +1,10 @@
 void inplace_double (int *p)
 /* --BEGIN-- */
-/*@ requires take n_ = Owned<int>(p);
-             let r = 2i64 * ((i64) n_);
-             (i64)MINi32() <= r; r <= (i64)MAXi32();
-    ensures  take m_ = Owned<int>(p);
-             m_ == (i32) r;
+/*@ requires take P = Owned<int>(p);
+             let M = 2i64 * ((i64) P);
+             (i64) MINi32() <= M; M <= (i64) MAXi32();
+    ensures  take P_post = Owned<int>(p);
+             P_post == (i32) M;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/slf8_basic_transfer.c b/src/examples/slf8_basic_transfer.c
index ffa37489..71a80c6a 100644
--- a/src/examples/slf8_basic_transfer.c
+++ b/src/examples/slf8_basic_transfer.c
@@ -1,11 +1,11 @@
 void transfer (unsigned int *p, unsigned int *q)
 /* --BEGIN-- */
-/*@ requires take n1 = Owned(p);
-             take m1 = Owned(q);
-    ensures  take n2 = Owned(p);
-             take m2 = Owned(q);
-             n2 == n1 + m1;
-             m2 == 0u32;
+/*@ requires take P = Owned(p);
+             take Q = Owned(q);
+    ensures  take P_post = Owned(p);
+             take Q_post = Owned(q);
+             P_post == P + Q;
+             Q_post == 0u32;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/slf_incr2.c b/src/examples/slf_incr2.c
index 94de75c6..43e99c3f 100644
--- a/src/examples/slf_incr2.c
+++ b/src/examples/slf_incr2.c
@@ -1,25 +1,25 @@
 /*@
-predicate { u32 pv, u32 qv } BothOwned (pointer p, pointer q)
+predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q)
 {
   if (ptr_eq(p,q)) {
-    take pv = Owned<unsigned int>(p);
-    return {pv: pv, qv: pv};
+    take PX = Owned<unsigned int>(p);
+    return {P: PX, Q: PX};
   }
   else {
-    take pv = Owned<unsigned int>(p);
-    take qv = Owned<unsigned int>(q);
-    return {pv: pv, qv: qv};
+    take PX = Owned<unsigned int>(p);
+    take QX = Owned<unsigned int>(q);
+    return {P: PX, Q: QX};
   }
 }
 @*/
 
 void incr2 (unsigned int *p, unsigned int *q)
-/*@ requires take vs = BothOwned(p,q);
-    ensures take vs_ = BothOwned(p,q);
-            ptr_eq (vs_.pv,
-                    (!ptr_eq(p,q)) ? (vs.pv + 1u32) : (vs.pv + 2u32));
-            ptr_eq (vs_.qv,
-                    (!ptr_eq(p,q)) ? (vs.qv + 1u32) : vs_.pv);
+/*@ requires take PQ = BothOwned(p,q);
+    ensures take PQ_post = BothOwned(p,q);
+            ptr_eq (PQ_post.P,
+                    (!ptr_eq(p,q)) ? (PQ.P + 1u32) : (PQ.P + 2u32));
+            ptr_eq (PQ_post.Q,
+                    (!ptr_eq(p,q)) ? (PQ.Q + 1u32) : PQ_post.P);
 @*/
 {
   /*@ split_case ptr_eq(p,q); @*/
@@ -32,13 +32,13 @@ void incr2 (unsigned int *p, unsigned int *q)
 }
 
 void call_both_better (unsigned int *p, unsigned int *q)
-/*@ requires take pv = Owned<unsigned int>(p);
-             take qv = Owned<unsigned int>(q);
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
              !ptr_eq(p,q);
-    ensures take pv_ = Owned<unsigned int>(p);
-            take qv_ = Owned<unsigned int>(q);
-            pv_ == pv + 3u32;
-            qv_ == qv + 1u32;
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 3u32;
+            Q_post == Q + 1u32;
 @*/
 {
   incr2(p, q);
diff --git a/src/examples/slf_incr2_alias.c b/src/examples/slf_incr2_alias.c
index 2eff193b..2f8cd75c 100644
--- a/src/examples/slf_incr2_alias.c
+++ b/src/examples/slf_incr2_alias.c
@@ -1,9 +1,28 @@
+// Increment two different pointers (same as above)
+void incr2a (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 1u32;
+            Q_post == Q + 1u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  *p = m;
+  n = *q;
+  m = n+1;
+  *q = m;
+}
+
+// Increment the same pointer twice
 void incr2b (unsigned int *p, unsigned int *q)
-/*@ requires take pv = Owned<unsigned int>(p);
+/*@ requires take P = Owned<unsigned int>(p);
              ptr_eq(q,p);
-    ensures take pv_ = Owned<unsigned int>(p);
+    ensures take P_post = Owned<unsigned int>(p);
             ptr_eq(q,p);
-            pv_ == pv + 2u32;
+            P_post == P + 2u32;
 @*/
 {
   unsigned int n = *p;
@@ -14,8 +33,6 @@ void incr2b (unsigned int *p, unsigned int *q)
   *q = m;
 }
 
-#include "slf_incr2_noalias.c"
-
 void call_both (unsigned int *p, unsigned int *q)
 /*@ requires take pv = Owned<unsigned int>(p);
              take qv = Owned<unsigned int>(q);
@@ -25,6 +42,6 @@ void call_both (unsigned int *p, unsigned int *q)
             qv_ == qv + 1u32;
 @*/
 {
-  incr2a(p, q);
-  incr2b(p, p);
+  incr2a(p, q);   // increment two different pointers
+  incr2b(p, p);   // increment the same pointer twice
 }
diff --git a/src/examples/slf_incr2_noalias.c b/src/examples/slf_incr2_noalias.c
index d4966069..7c7e2369 100644
--- a/src/examples/slf_incr2_noalias.c
+++ b/src/examples/slf_incr2_noalias.c
@@ -1,10 +1,10 @@
 void incr2a (unsigned int *p, unsigned int *q)
-/*@ requires take pv = Owned<unsigned int>(p);
-             take qv = Owned<unsigned int>(q);
-    ensures take pv_ = Owned<unsigned int>(p);
-            take qv_ = Owned<unsigned int>(q);
-            pv_ == pv + 1u32;
-            qv_ == qv + 1u32;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 1u32;
+            Q_post == Q + 1u32;
 @*/
 {
   unsigned int n = *p;
diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c
index 34d85294..27e919bd 100644
--- a/src/examples/slf_length_acc.c
+++ b/src/examples/slf_length_acc.c
@@ -3,25 +3,25 @@
 #include "free.h"
 
 /*@
-function [rec] (u32) length(datatype seq xs) {
+function [rec] (u32) length(datatype List xs) {
   match xs {
-    Seq_Nil {} => {
+    Nil {} => {
       0u32
     }
-    Seq_Cons {head : h, tail : zs}  => {
+    Cons {Head: h, Tail: zs}  => {
       1u32 + length(zs)
     }
   }
 }
 @*/
 
-void IntList_length_acc_aux (struct int_list *xs, unsigned int *p)
-/*@ requires take L1 = IntList(xs);
-             take n = Owned<unsigned int>(p);
-    ensures take L1_ = IntList(xs);
-            take n_ = Owned<unsigned int>(p);
-            L1 == L1_;
-            n_ == n + length(L1);
+void IntList_length_acc_aux (struct sllist *xs, unsigned int *p)
+/*@ requires take L1 = SLList(xs);
+             take P = Owned<unsigned int>(p);
+    ensures take L1_post = SLList(xs);
+            take P_post = Owned<unsigned int>(p);
+            L1 == L1_post;
+            P_post == P + length(L1);
 @*/
 {
   /*@ unfold length(L1); @*/
@@ -32,11 +32,11 @@ void IntList_length_acc_aux (struct int_list *xs, unsigned int *p)
   }
 }
 
-unsigned int IntList_length_acc (struct int_list *xs)
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            L1 == L1_;
-            return == length(L1);
+unsigned int IntList_length_acc (struct sllist *xs)
+/*@ requires take Xs = SLList(xs);
+    ensures take Xs_post = SLList(xs);
+            Xs == Xs_post;
+            return == length(Xs);
 @*/
 {
   unsigned int *p = refUnsignedInt(0);
diff --git a/src/examples/slf_quadruple_mem.c b/src/examples/slf_quadruple_mem.c
index 0c7e647b..c7a86dc3 100644
--- a/src/examples/slf_quadruple_mem.c
+++ b/src/examples/slf_quadruple_mem.c
@@ -1,11 +1,11 @@
 int quadruple_mem (int *p)
 /* --BEGIN-- */
-/*@ requires take n = Owned<int>(p);
-             let n_ = (i64) n;
-             (i64)MINi32() <= n_ * 4i64; n_ * 4i64 <= (i64)MAXi32();
-    ensures take n2 = Owned<int>(p);
-            n2 == n;
-            return == 4i32 * n;
+/*@ requires take P = Owned<int>(p);
+             let P64 = (i64) P;
+             (i64)MINi32() <= P64 * 4i64; P64 * 4i64 <= (i64)MAXi32();
+    ensures take P_post = Owned<int>(p);
+            P_post == P;
+            return == 4i32 * P;
  @*/
 /* --END-- */
 {
diff --git a/src/examples/slf_ref_greater.c b/src/examples/slf_ref_greater.c
index 23c54c9c..96138e91 100644
--- a/src/examples/slf_ref_greater.c
+++ b/src/examples/slf_ref_greater.c
@@ -2,12 +2,12 @@
 
 unsigned int *ref_greater_abstract (unsigned int *p)
 /* --BEGIN-- */
-/*@ requires take m1 = Owned<unsigned int>(p);
-             m1 < 4294967295u32;
-    ensures take m2 = Owned<unsigned int>(p);
-            take n2 = Owned<unsigned int>(return);
-            m1 == m2;
-            m1 <= n2;
+/*@ requires take P = Owned<unsigned int>(p);
+             P < 4294967295u32;
+    ensures take P_post = Owned<unsigned int>(p);
+            take R = Owned<unsigned int>(return);
+            P == P_post;
+            P <= R;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c
index a258057d..6958ca70 100644
--- a/src/examples/slf_sized_stack.c
+++ b/src/examples/slf_sized_stack.c
@@ -3,114 +3,113 @@
 
 struct sized_stack {
   unsigned int size;
-  struct int_list* data;
+  struct sllist* data;
 };
 
 /*@
-type_synonym sizeAndData = {u32 s, datatype seq d}
+type_synonym SizedStack = {u32 Size, datatype List Data}
 
-predicate (sizeAndData) SizedStack(pointer p) {
-    take S = Owned<struct sized_stack>(p);
-    let s = S.size;
-    take d = IntList(S.data);
-    assert(s == length(d));
-    return { s: s, d: d };
+predicate (SizedStack) SizedStack (pointer p) {
+    take P = Owned<struct sized_stack>(p);
+    take D = SLList(P.data);
+    assert(P.size == Length(D));
+    return { Size: P.size, Data: D };
 }
 @*/
 
-extern struct sized_stack *malloc_sized_stack ();
+extern struct sized_stack *malloc__sized_stack ();
 /*@
-spec malloc_sized_stack();
+spec malloc__sized_stack();
      requires true;
-     ensures take u = Block<struct sized_stack>(return);
+     ensures take R = Block<struct sized_stack>(return);
 @*/
 
-extern void *free_sized_stack (struct sized_stack *p);
+extern void *free__sized_stack (struct sized_stack *s);
 /*@
-spec free_sized_stack(pointer p);
-     requires take u = Block<struct sized_stack>(p);
+spec free__sized_stack(pointer s);
+     requires take R = Block<struct sized_stack>(s);
      ensures true;
 @*/
 
 struct sized_stack* create()
-/*@ ensures take S = SizedStack(return);
-            S.s == 0u32;
+/*@ ensures take R = SizedStack(return);
+            R.Size == 0u32;
 @*/
 {
-  struct sized_stack *p = malloc_sized_stack();
-  p->size = 0;
-  p->data = 0;
-  /*@ unfold length(Seq_Nil {}); @*/
-  return p;
+  struct sized_stack *s = malloc__sized_stack();
+  s->size = 0;
+  s->data = 0;
+  /*@ unfold Length(Nil {}); @*/
+  return s;
 }
 
-unsigned int sizeOf (struct sized_stack *p)
+unsigned int sizeOf (struct sized_stack *s)
 /* FILL IN HERE */
 /* ---BEGIN--- */
-/*@ requires take S = SizedStack(p);
-    ensures take S_ = SizedStack(p);
-            S_ == S;
-            return == S.s;
+/*@ requires take S = SizedStack(s);
+    ensures take S_post = SizedStack(s);
+            S_post == S;
+            return == S.Size;
 @*/
 /* ---END--- */
 {
-  return p->size;
+  return s->size;
 }
 
-void push (struct sized_stack *p, int x)
+void push (struct sized_stack *s, int x)
 /* FILL IN HERE */
 /* ---BEGIN--- */
-/*@ requires take S = SizedStack(p);
-    ensures take S_ = SizedStack(p);
-            S_.d == Seq_Cons {head:x, tail:S.d};
+/*@ requires take S = SizedStack(s);
+    ensures take S_post = SizedStack(s);
+            S_post.Data == Cons {Head:x, Tail:S.Data};
 @*/
 /* ---END--- */
 {
-  struct int_list *data = IntList_cons(x, p->data);
-  p->size++;
-  p->data = data;
+  struct sllist *data = slcons(x, s->data);
+  s->size++;
+  s->data = data;
 /* ---BEGIN--- */
-  /*@ unfold length (Seq_Cons {head: x, tail: S.d}); @*/
+  /*@ unfold Length (Cons {Head: x, Tail: S.Data}); @*/
 /* ---END--- */
 }
 
-int pop (struct sized_stack *p)
+int pop (struct sized_stack *s)
 /* FILL IN HERE */
 /* ---BEGIN--- */
-/*@ requires take S = SizedStack(p);
-             S.s > 0u32;
-    ensures  take S_ = SizedStack(p);
-             S_.d == tl(S.d);
+/*@ requires take S = SizedStack(s);
+             S.Size > 0u32;
+    ensures  take S_post = SizedStack(s);
+             S_post.Data == Tl(S.Data);
 @*/
 /* ---END--- */
 {
-  struct int_list *data = p->data;
+  struct sllist *data = s->data;
   if (data != 0) {
     int head = data->head;
-    struct int_list *tail = data->tail;
-    freeIntList(data);
-    p->data = tail;
-    p->size--;
+    struct sllist *tail = data->tail;
+    free__sllist(data);
+    s->data = tail;
+    s->size--;
 /* ---BEGIN--- */
-    /*@ unfold length(S.d); @*/
+    /*@ unfold Length(S.Data); @*/
 /* ---END--- */
     return head;
   }
   return 42;
 }
 
-int top (struct sized_stack *p)
-/*@ requires take S = SizedStack(p);
-             S.s > 0u32;
-    ensures  take S_ = SizedStack(p);
-             S_ == S;
-             return == hd(S.d);
+int top (struct sized_stack *s)
+/*@ requires take S = SizedStack(s);
+             S.Size > 0u32;
+    ensures  take S_post = SizedStack(s);
+             S_post == S;
+             return == Hd(S.Data);
 @*/
 {
-  /*@ unfold length(S.d); @*/ 
-  // from S.s > 0u32 it follows that the 'else' branch is impossible
-  if (p->data != 0) {
-    return (p->data)->head;
+  /*@ unfold Length(S.Data); @*/ 
+  // from S.Size > 0u32 it follows that the 'else' branch is impossible
+  if (s->data != 0) {
+    return (s->data)->head;
   }
   else {
     // provably dead code
diff --git a/src/examples/swap.c b/src/examples/swap.c
index 31a8c119..435ef1b0 100644
--- a/src/examples/swap.c
+++ b/src/examples/swap.c
@@ -1,10 +1,10 @@
 void swap (unsigned int *p, unsigned int *q)
 /* --BEGIN-- */
-/*@ requires take v = Owned<unsigned int>(p);
-             take w = Owned<unsigned int>(q);
-    ensures  take v2 = Owned<unsigned int>(p);
-             take w2 = Owned<unsigned int>(q);
-             v2 == w && w2 == v;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures  take P_post = Owned<unsigned int>(p);
+             take Q_post = Owned<unsigned int>(q);
+             P_post == Q && Q_post == P;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/transpose.broken.c b/src/examples/transpose.broken.c
index 3bb2ca95..47ef9479 100644
--- a/src/examples/transpose.broken.c
+++ b/src/examples/transpose.broken.c
@@ -1,10 +1,10 @@
 struct point { int x; int y; };
 
 void transpose (struct point *p) 
-/*@ requires take s = Owned<struct point>(p); 
-    ensures take s2 = Owned<struct point>(p); 
-            s2.x == s.y;
-            s2.y == s.x; 
+/*@ requires take P = Owned<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
 @*/
 {
   int temp_x = p->x;
diff --git a/src/examples/transpose.c b/src/examples/transpose.c
index 5bab82bf..03b1d9d8 100644
--- a/src/examples/transpose.c
+++ b/src/examples/transpose.c
@@ -1,10 +1,10 @@
 struct point { int x; int y; };
 
 void transpose (struct point *p) 
-/*@ requires take s = Owned<struct point>(p);
-    ensures take s2 = Owned<struct point>(p);
-            s2.x == s.y;
-            s2.y == s.x;
+/*@ requires take P = Owned<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
 @*/
 {
   int temp_x = p->x;
diff --git a/src/examples/transpose2.c b/src/examples/transpose2.c
index 6a903ad3..31b390fd 100644
--- a/src/examples/transpose2.c
+++ b/src/examples/transpose2.c
@@ -1,9 +1,9 @@
 void swap (unsigned int *p, unsigned int *q)
-/*@ requires take v = Owned<unsigned int>(p);
-             take w = Owned<unsigned int>(q);
-    ensures  take v2 = Owned<unsigned int>(p);
-             take w2 = Owned<unsigned int>(q);
-             v2 == w && w2 == v;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures  take P_post = Owned<unsigned int>(p);
+             take Q_post = Owned<unsigned int>(q);
+             P_post == Q && Q_post == P;
 @*/
 {
   unsigned int m = *p;
@@ -16,12 +16,12 @@ struct upoint { unsigned int x; unsigned int y; };
 
 void transpose2 (struct upoint *p)
 /* --BEGIN-- */
-/*@ requires take s = Owned<struct upoint>(p);
-    ensures take s2 = Owned<struct upoint>(p);
-            s2.x == s.y;
-            s2.y == s.x;
+/*@ requires take P = Owned<struct upoint>(p);
+    ensures take P_post = Owned<struct upoint>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
 @*/
+/* --END-- */
 {
   swap(&p->x, &p->y);
 }
-/* --END-- */
diff --git a/src/examples/zero.c b/src/examples/zero.c
index e6ac6cdd..c7fbf8c7 100644
--- a/src/examples/zero.c
+++ b/src/examples/zero.c
@@ -1,8 +1,8 @@
 void zero (int *p)
 /* --BEGIN-- */
-/*@ requires take u = Block<int>(p);
-    ensures take v = Owned<int>(p);
-            v == 0i32;
+/*@ requires take P = Block<int>(p);
+    ensures take P_post = Owned<int>(p);
+            P_post == 0i32;
 @*/
 /* --END-- */
 {
diff --git a/src/queue-example-notes.md b/src/queue-example-notes.md
index 09eb24c9..f2d39a56 100644
--- a/src/queue-example-notes.md
+++ b/src/queue-example-notes.md
@@ -1,8 +1,8 @@
 2# Notes
 
-- Bad definition of snoc (same as rev). How to spot? Look at constraint context, specifically snoc(listQ, x) == match listQ {Seq\_Nil {} => {Seq\_Nil {}}Seq\_Cons {head: h, tail: zs} => {snoc(rev(zs), h)}}. Other big clue: applying lemma snoc_nil results in an inconsistent context. This is really nasty because snoc(Seq_Nil{}, x) ends up reducing to itself.
+- Bad definition of snoc (same as rev). How to spot? Look at constraint context, specifically snoc(listQ, x) == match listQ {Seq\_Nil {} => {Seq\_Nil {}}Seq\_Cons {Head: h, Tail: zs} => {snoc(rev(zs), h)}}. Other big clue: applying lemma snoc_nil results in an inconsistent context. This is really nasty because snoc(Nil{}, x) ends up reducing to itself.
 
-- Code used q->tail == 0 but predicate was testing q->head. Can adjust predicate, code, or use a split_case.
+- Code used q->tail == 0 but predicate was testing q->Head. Can adjust predicate, code, or use a split_case.
 
 - Under-constrained counter-examples are something to be aware of (though the inconsitency came because of the definition of snoc here rather than l here).
 
@@ -22,37 +22,37 @@ More notes:
 
 Here's the predicate for queues:
 
-    predicate (datatype seq) IntQueue(pointer q) {
+    predicate (datatype List) IntQueue(pointer q) {
       take H = Owned<struct int_queue>(q);
       take Q = IntQueue1(q,H);
       return Q;
     }
 
-    predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) {
-      if (is_null(H.head)) {
+    predicate (datatype List) IntQueue1(pointer dummy, struct int_queue H) {
+      if (is_null(H.Head)) {
         assert (is_null(H.tail));
-        return (Seq_Nil{});
+        return (Nil{});
       } else {
         assert (!is_null(H.tail));
-        take Q = IntQueueAux (H.head, H.tail);
+        take Q = IntQueueAux (H.Head, H.tail);
         return Q;
       }
     }
 
-    predicate (datatype seq) IntQueueAux(pointer h, pointer t) {
+    predicate (datatype List) IntQueueAux(pointer h, pointer t) {
       take C = Owned<struct int_queueCell>(h);
       take L = IntQueueAux1(h, C, t);
       return L;
     }
 
-    predicate (datatype seq) IntQueueAux1
+    predicate (datatype List) IntQueueAux1
                                (pointer h, struct int_queueCell C, pointer t) {
       if (is_null(C.next)) {
         assert (h == t);
-        return (Seq_Cons{head: C.first, tail: Seq_Nil{}});
+        return (Cons{Head: C.first, Tail: Nil{}});
       } else {
         take TL = IntQueueAux(C.next, t);
-        return (Seq_Cons { head: C.first, tail: TL });
+        return (Cons { Head: C.first, Tail: TL });
       }
     }
 
@@ -80,11 +80,11 @@ This fails because there are not enough annotations in the body of push.
 
 Confusingly, the HTML error report gives this as the unproven constraint
 
-    Seq_Cons {head: x, tail: Seq_Nil {}} == snoc(l, x)
+    Cons {Head: x, Tail: Nil {}} == snoc(l, x)
 
 while the list of Terms shows that
 
-    Seq_Cons {head: x, tail: Seq_Nil {}} == snoc(l, x)
+    Cons {Head: x, Tail: Nil {}} == snoc(l, x)
 
 has value false!
 
@@ -111,7 +111,7 @@ not, so even to look "one level deep" we need an unfold.)
 
 Once we've unfolded, we get some more hints:
 
-  - Look at the value of l in Terms: Seq_Cons {head: 0i32, tail: Seq_Nil {}}
+  - Look at the value of l in Terms: Cons {Head: 0i32, Tail: Nil {}}
   - But we are in the empty queue case, so this seems fishy.
   - Now, in the constraints, we see   l == unpack_IntQueue1.Q
   - Then look at the resources and see that unpack_IntQueue1.Q has not
@@ -119,7 +119,7 @@ Once we've unfolded, we get some more hints:
         IntQueue1(q, unpack_IntQueue1.H)(unpack_IntQueue1.Q)
   - This means that CN did not have enough information to decide which
     way the conditional at the beginning of IntQueue1 is going to go.
-  - But the condition is testing H.head, while the conditional in the
+  - But the condition is testing H.Head, while the conditional in the
     code is testing the tail field!
   - We could get around this mismatch by adjusting the condition
     itself, or by adjusting the predicate.  E.g., we could change the
@@ -128,12 +128,12 @@ Once we've unfolded, we get some more hints:
 
 This tells us to look at snoc, which turns out to be very wrong!
 
-    function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
+    function [rec] (datatype List) snoc(datatype List xs, i32 y) {
       match xs {
-        Seq_Nil {} => {
-          Seq_Nil {}
+        Nil {} => {
+          Nil {}
         }
-        Seq_Cons {head : h, tail : zs}  => {
+        Cons {Head : h, Tail : zs}  => {
           snoc (rev(zs), h)
         }
       }
@@ -189,32 +189,32 @@ Instead, we need to rearrange IntQueue and friends so that we take
 ownership of the very last cell in the list at the very beginning,
 instead of at the very end.
 
-    predicate (datatype seq) IntQueue(pointer q) {
+    predicate (datatype List) IntQueue(pointer q) {
       take H = Owned<struct int_queue>(q);
       take Q = IntQueue1(q,H);
       return Q;
     }
 
-    predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) {
-      if (is_null(H.head)) {
+    predicate (datatype List) IntQueue1(pointer dummy, struct int_queue H) {
+      if (is_null(H.Head)) {
         assert (is_null(H.tail));
-        return (Seq_Nil{});
+        return (Nil{});
       } else {
         assert (!is_null(H.tail));
         take T = Owned<struct int_queueCell>(H.tail);
         assert (is_null(T.next));
-        take Q = IntQueueAux (H.head, H.tail, T.first);
+        take Q = IntQueueAux (H.Head, H.tail, T.first);
         return Q;
       }
     }
 
-    predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) {
+    predicate (datatype List) IntQueueAux (pointer h, pointer t, i32 lastVal) {
       if (h == t) {
-        return (Seq_Cons{head: lastVal, tail: Seq_Nil{}});
+        return (Cons{Head: lastVal, Tail: Nil{}});
       } else {
         take C = Owned<struct int_queueCell>(h);
         take TL = IntQueueAux(C.next, t, lastVal);
-        return (Seq_Cons { head: C.first, tail: TL });
+        return (Cons { Head: C.first, Tail: TL });
       }
     }
 
diff --git a/src/tutorial.adoc b/src/tutorial.adoc
index e641a65c..f2996ed6 100644
--- a/src/tutorial.adoc
+++ b/src/tutorial.adoc
@@ -10,11 +10,13 @@ By Christopher Pulte and Benjamin C. Pierce, with contributions from Elizabeth A
 
 [abstract]
 --
-CN is a type system for verifying C code, focusing especially on low-level systems code. Compared to the normal C type system, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — according to strong user-defined specifications. 
-// 
-This tutorial introduces CN along a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures. 
+CN is an extension of the C programming language for verifying the correctness of C code, especially on low-level systems code. Compared to standard C, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — satisfying to strong, user-defined specifications. 
+This tutorial introduces CN through a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures. 
 
-CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami.
+This tutorial is a work in progress -- your suggestions are greatly appreciated!
+
+**Origins.**
+CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami.
 //
 To accurately handle the complex semantics of C, CN builds on the https://github.com/rems-project/cerberus/[Cerberus semantics for C].
 //
@@ -23,8 +25,6 @@ https://softwarefoundations.cis.upenn.edu[Separation Logic
 Foundations] textbook, and one of the case studies is based on an
 extended exercise due to Bryan Parno.
 
-This tutorial is a work in progress -- your suggestions are greatly appreciated!
-
 **Acknowledgment of Support and Disclaimer.**
 This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google.  The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
 
@@ -32,46 +32,42 @@ This material is based upon work supported by the Air Force Research Laboratory
 
 == Installing CN
 
-To fetch and install CN, check the Cerberus repository at https://github.com/rems-project/cerberus and follow the instructions in https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md[backend/cn/README.md].
+To fetch and install CN, visit the Cerberus repository at https://github.com/rems-project/cerberus and follow the instructions in https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md[backend/cn/README.md].
 
-Once completed, type `+cn --help+` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with.
+Once the installation is completed, type `+cn --help+` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with.
 
-To apply CN to a C file, run `+cn CFILE+`.
+To apply CN to a C file, run `+cn verify CFILE+`.
 
-== Source files for the exercises and examples
+== Source files
 
-The source files can be downloaded from link:exercises.zip[here].
+The source files for all the exercises and examples below can be downloaded
+from link:exercises.zip[here].
 
-== Basic usage
+== Basics
 
 === First example
 
-For a first example, let’s look at a simple arithmetic function: `+add+`, shown below, takes two `+int+` arguments, `+x+` and `+y+`, and returns their sum.
+The simple arithmetic function: `+add+` shown below takes two `+int+` arguments, `+x+` and `+y+`, and returns their sum.
 
-// TODO: BCP: We should probably adopt the convention that all the files in
-// the exercises directory have a comment at the top giving their name.
-// (We could actually auto-generate those header comments when we process
-// /src/examples into build/exercises, to avoid having to maintain them
-// and possibly get them wrong...)
 include_example(exercises/add_0.c)
 
 Running CN on the example produces an error message:
 
 ....
-cn exercises/add_0.c
+cn verify exercises/add_0.c
 [1/1]: add
 exercises/add_0.c:3:10: error: Undefined behaviour
   return x+y;
          ~^~
 an exceptional condition occurs during the evaluation of an expression (§6.5#5)
-Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_393431.html
+Consider the state in /var/folders/_v/ndl32rvc8ph0000gn/T/state_393431.html
 ....
 
-CN rejects the program because it has _C undefined behaviour_, meaning it is not safe to execute. CN points to the relevant source location, the addition `+x+y+`, and paragraph §6.5#5 of the C language standard that specifies the undefined behaviour. It also puts a link to an HTML file with more details on the error to help in diagnosing the problem.
+CN rejects the program because it has _undefined behaviour_ according to the C standard, meaning it is not safe to execute. CN points to the relevant source location, the addition `+x+y+`, and paragraph §6.5#5 of the standard, which specifies the undefined behaviour. It also includes a link to an HTML file with more details on the error to help in diagnosing the problem.
 
 Inspecting this HTML report (as we do in a moment) gives us possible example values for `+x+` and `+y+` that cause the undefined behaviour and hint at the problem: for very large values for `+x+` and `+y+`, such as `+1073741825+` and `+1073741824+`, the sum of `+x+` and `+y+` can exceed the representable range of a C `+int+` value: `+1073741825 + 1073741824 = 2^31+1+`, so their sum is larger than the maximal `+int+` value, `+2^31-1+`.
 
-Here `+x+` and `+y+` are _signed integers_, and in C, signed integer _overflow_ is undefined behaviour (UB). Hence, `+add+` is only safe to execute for smaller values. Similarly, _large negative_ values of `+x+` and `+y+` can cause signed integer _underflow_, also UB in C. We therefore need to rule out too large values for `+x+` and `+y+`, both positive and negative, which we do by writing a CN function specification.
+Here `+x+` and `+y+` are _signed integers_, and in C, signed integer _overflow_ is undefined behaviour (UB). Hence, `+add+` is only safe to execute for smaller values. Similarly, _large negative_ values of `+x+` and `+y+` can cause signed integer _underflow_, also UB in C. We therefore need to rule out too-large values for `+x+` and `+y+`, both positive and negative, which we do by writing a CN function specification.
 
 === First function specification
 
@@ -89,22 +85,27 @@ In detail:
 
 * In function specifications, the names of the function arguments, here `+x+` and `+y+`, refer to their _initial values_. (Function arguments are mutable in C.)
 
-* `+let sum = (i64) x + (i64) y+` is a let-binding, which defines `+sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification.
+* `+let Sum = (i64) x + (i64) y+` is a let-binding, which defines `+Sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification.
 
-* Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`.
+* Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers, to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`.
 // TODO: BCP: I understand this reasoning, but I wonder whether it introduces more confusion than it avoids -- it means there are two ways of writing everything, and people have to remember whether the particular thing they are writing right now is C or CN...
+// TODO: BCP: Hopefully we are moving toward unifying these notations anyway?
 
-* To define `+sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values.
+* To define `+Sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values.
 
-* Finally, we require this sum to be in-between the minimal and maximal `+int+` value. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`).
+* Finally, we require this sum to be between the minimal and maximal `+int+` values. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`).
+// TODO: BCP: We should use the new ' syntax (or whatever it turned out to be) for numeric constants
 
-Running CN on the annotated program passes without errors. This means with our specified precondition, `+add+` is safe to execute.
+Running CN on the annotated program passes without errors. This means that, with our specified precondition, `+add+` is safe to execute.
 
-We may, however, wish to be more precise. So far the specification gives no information to callers of `+add+` about its output. To also specify the return values we add a postcondition, using the `+ensures+` keyword.
+We may, however, wish to be more precise. So far, the specification gives no information to callers of `+add+` about its output. To describe its return value we add a postcondition to the specification using the `+ensures+` keyword.
 
 include_example(solutions/add_1.c)
 
-Here we use the keyword `+return+`, only available in function postconditions, to refer to the return value, and equate it to `+sum+` as defined in the preconditions, cast back to `+i32+` type: `+add+` returns the sum of `+x+` and `+y+`.
+Here we use the keyword `+return+`, which is only available in function
+postconditions, to refer to the return value, and we equate it to `+Sum+`
+as defined in the precondition, cast back to `+i32+` type: that is, `+add+`
+returns the sum of `+x+` and `+y+`.
 
 Running CN confirms that this postcondition also holds.
 
@@ -112,51 +113,96 @@ One final refinement of this example.  CN defines constant functions `MINi32`, `
 
 include_example(solutions/add_2.c)
 
-Two things to note:
-   * These are constant _functions_, so they require a following `()`.
-   * The type of `MINi32()` is `i32`, so if we want to use it as a 64-bit constant
-     we need to add the explicit coercion `(i64)`.
+Two things to note: (1) These are constant _functions_, so they
+require a following `()`.  And (2) The type of `MINi32()` is `i32`, so
+if we want to use it as a 64-bit constant we need to add the explicit
+coercion `(i64)`.
 
 === Error reports
 
-In the original example CN reported a type error due to C undefined behaviour. While that example was perhaps simple enough to guess the problem and solution, this can become quite challenging as program and specification complexity increases. Diagnosing type errors is therefore an important part of using CN. CN tries to help with that by producing detailed error information, in the form of an HTML error report.
+In the original example, CN reported a type error due to C undefined
+behaviour. While that example was perhaps simple enough to guess the
+problem and solution, this can become quite challenging as program and
+specification complexity increases. Diagnosing errors is
+therefore an important part of using CN. CN tries to help with this by
+producing detailed error information, in the form of an HTML error
+report.
 
-Let’s return to the type error from earlier (`+add+` without precondition) and take a closer look at this report. The report comprises two sections.
+Let’s return to the type error from earlier -- `+add+` without
+precondition -- and take a closer look at this report. It
+comprises two sections:
 
-// TODO: BCP: It looks different now!
+// TODO: BCP: It looks quite different now!
 .*CN error report*
 image::images/0.error.png[*CN error report*]
 
-*Path.* The first section, "`Path to error`", contains information about the control-flow path leading to the error.
+*Path to error.* The first section contains information about the
+control-flow path leading to the error.
 
-When type checking a C function, CN checks each possible control-flow path through the program individually. If CN detects UB or a violation of user-defined specifications, CN reports the problematic control-flow path, as a nested structure of statements: paths are split into sections, which group together statements between high-level control-flow positions (e.g. function entry, the start of a loop, the invocation of a `+continue+`, `+break+`, or `+return+` statement, etc.); within each section, statements are listed by source code location; finally, per statement, CN lists the typechecked sub-expressions, and the memory accesses and function calls within these.
+When checking a C function, CN examines each possible control-flow
+path individually. If it detects UB or a violation of user-defined
+specifications, CN reports the problematic control-flow path as a
+nested structure of statements: the path is split into sections that
+group together statements between high-level control-flow positions
+(e.g. function entry, the start of a loop, the invocation of a
+`+continue+`, `+break+`, or `+return+` statement, etc.); within each
+section, statements are listed by source code location; finally, per
+statement, CN lists the typechecked sub-expressions, and the memory
+accesses and function calls within these.
 
 In our example, there is only one possible control-flow path: entering the function body (section "`function body`") and executing the block from lines 2 to 4, followed by the return statement at line 3. The entry for the latter contains the sequence of sub-expressions in the return statement, including reads of the variables `+x+` and `+y+`.
 
-In C, local variables in a function, including its arguments, are mutable and their address can be taken and passed as a value. CN therefore represents local variables as memory allocations that are manipulated using memory reads and writes. Here, type checking the return statement includes checking memory reads for `+x+` and `+y+`, at their locations `+&ARG0+` and `+&ARG1+`. The path report lists these reads and their return values: the read at `+&ARG0+` returns `+x+` (that is, the value of `+x+` originally passed to `+add+`); the read at `+&ARG1+` returns `+y+`. Alongside this symbolic information, CN displays concrete values:
+In C, local variables in a function, including its arguments, are
+mutable,  their addresses can be taken and passed as values. CN
+therefore represents local variables as memory allocations that are
+manipulated using memory reads and writes. Here, type checking the
+return statement includes checking memory reads for `+x+` and `+y+`,
+at their locations `+&ARG0+` and `+&ARG1+`. The path report lists
+these reads and their return values: the read at `+&ARG0+` returns
+`+x+` (that is, the value of `+x+` originally passed to `+add+`); the
+read at `+&ARG1+` returns `+y+`. Alongside this symbolic information,
+CN displays concrete values:
+// TODO: BCP: WHere do we see that ARG0 and ARG1 have something to do with x and y?
 
 * `+1073741825i32 /* 0x40000001 */+` for x (the first value is the decimal representation, the second, in `+/*...*/+` comments, the hex equivalent) and
 
 * `+1073741824i32 /* 0x40000000 */+` for `+y+`.
 
 For now, ignore the pointer values `+{@0; 4}+` for `+x+` and `+{@0; 0}+` for `+y+`.
+// TODO: BCP: Where are these things discussed?  Anywhere?  (When) are they useful?
 
-These concrete values are part of a _counterexample_: a concrete valuation of variables and pointers in the program that that leads to the error. (The exact values may vary on your machine, depending on the version of Z3 installed on your system.)
+These concrete values are part of a _counterexample_: a concrete
+valuation of variables and pointers in the program that that leads to
+the error. (The exact values may vary on your machine, depending on
+the SMT solver -- i.e., the particular version of Z3, CVC5, or
+whatever installed on your system.)
 
 *Proof context.* The second section, below the error trace, lists the proof context CN has reached along this control-flow path.
 
 "`Available resources`" lists the owned resources, as discussed in later sections.
 
 "`Variables`" lists counterexample values for program variables and pointers. In addition to `+x+` and `+y+`, assigned the same values as above, this includes values for their memory locations `+&ARG0+` and `+&ARG1+`, function pointers in scope, and the `+__cn_alloc_history+`, all of which we ignore for now.
+// TODO: BCP: Again, where are these things discussed?  Should they be?
 
-Finally, "`Constraints`" records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here (`+add+` without precondition) the only constraints are some contraints inferred from C-types in the code.
+Finally, "`Constraints`" records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here -- when checking `+add+` without precondition -- the only constraints are those inferred from C-types in the code:
 
-* For instance, `+good<signed int>(x)+` says that the initial value of `+x+` is a "`good`" `+signed int+` value (i.e. in range). Here `+signed int+` is the same type as `+int+`, CN just makes the sign explicit. For integer types `+T+`, `+good<T>+` requires the value to be in range of type `+T+`; for pointer types `+T+` it also requires the pointer to be aligned. For structs and arrays this extends in the obvious way to struct members or array cells.
+* For instance, `+good<signed int>(x)+` says that the initial value of
+`+x+` is a "`good`" `+signed int+` value (i.e. in range). Here
+`+signed int+` is the same type as `+int+`, CN just makes the sign
+explicit. 
+// TODO: BCP: Yikes!  This seems potentially cxonfusing
+For an integer type `+T+`, the type `+good<T>+` requires the value to
+be in range of type `+T+`; for pointer types `+T+`, it also requires
+the pointer to be aligned. For structs and arrays, this extends in the
+obvious way to struct members or array cells.
+// TODO: BCP: Is this information actually ever usefulful?  Is it currently suppressed?  
 
 * `+repr<T>+` requires representability (not alignment) at type `+T+`, so `+repr<signed int*>(&ARGO)+`, for instance, records that the pointer to `+x+` is representable at C-type `+signed int*+`;
 
 * `+aligned(&ARGO, 4u64)+`, moreover, states that it is 4-byte aligned.
 
+// TODO: BCP: Some of the above (especially the bit at the end) feels like TMI for many/most users, especially at this point in the tutorial.  
+
 === Another arithmetic example
 
 Let’s apply what we know so far to another simple arithmetic example.
@@ -168,15 +214,17 @@ include_example(exercises/slf1_basic_example_let.signed.c)
 
 We would like to verify this is safe, and that `+doubled+` returns twice the value of `+n+`. Running CN on `+doubled+` leads to a type error: the increment of `+a+` has undefined behaviour.
 
-As in the first example, we need to ensure that `+n+1+` does not overflow and `+n-1+` does not underflow. Similarly also `+a+b+` has to be representable at `+int+` type.
+As in the first example, we need to ensure that `+n+1+` does not overflow and `+n-1+` does not underflow. Similarly `+a+b+` has to be representable at `+int+` type.
 
 include_example(solutions/slf1_basic_example_let.signed.c)
+// TODO: BCP: WHy n_+n_ in some places and n*2i32 in others?
 
-We can specify these using a similar style of precondition as in the first example. We first define `+n_+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+` and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+n_+` does not go below the minimal `+int+` value, that incrementing `+n_+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution.
+We encode these expectations using a similar style of precondition as in the first example. We first define `+N+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+`, and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+N+` does not go below the minimal `+int+` value, that incrementing `+N+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution.
+// TODO: BCP: How about renaming N to n64?
 
 To capture the functional behaviour, the postcondition specifies that `+return+` is twice the value of `+n+`.
 
-=== Exercise
+=== Exercises
 
 *Quadruple.* Specify the precondition needed to ensure safety of the C function `+quadruple+`, and a postcondition that describes its return value.
 
@@ -190,6 +238,8 @@ include_example(exercises/abs.c)
 
 So far we’ve only considered example functions manipulating integer values. Verification becomes more interesting and challenging when _pointers_ are involved, because the safety of memory accesses via pointers has to be verified.
 
+// TODO: BCP: As a non-expert coming to CN, I was (and to some extent still am) consistently confused by the terminology of "resource TYPES" -- they do not look like types, and I just think of them as resources.  I think we could save other readers some confusion by reserving the word "type" for C-types and juset talking about "resources" for CN-level things.
+
 CN uses _separation logic resource types_ and the concept of _ownership_ to reason about memory accesses. A resource is the permission to access a region of memory. Unlike logical constraints, resource ownership is _unique_, meaning resources cannot be duplicated.
 
 Let’s look at a simple example. The function `+read+` takes an `+int+` pointer `+p+` and returns the pointee value.
@@ -199,7 +249,7 @@ include_example(exercises/read.c)
 Running CN on this example produces the following error:
 
 ....
-cn exercises/read.c
+cn verify exercises/read.c
 [1/1]: read
 exercises/read.c:3:10: error: Missing resource for reading
   return *p;
@@ -212,13 +262,15 @@ For the read `+*p+` to be safe, ownership of a resource is missing: a resource `
 
 === The Owned resource type
 
+// TODO: BCP: Perhaps this is a good time for one last discussion of the keyword "Owned", which I have never found very helpful: the resource itself isn't owned -- it's a description of something that *can* be owned.  (It's "take" that does the owning.)  Moreover, "Owned" and "Block" are badly non-parallel, both grammatically and semantically.  I suggest "Resource" instead of "Owned".  (We can keep "Block" -- it's not too bad, IMO.)
+
 Given a C-type `+T+` and pointer `+p+`, the resource `+Owned<T>(p)+` asserts ownership of a memory cell at location `+p+` of the size of C-type `+T+`. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types `+T+`).
 
-In this example we can ensure the safe execution of `+read+` by adding a precondition that requires ownership of `+Owned<int>(p)+`, as shown below. For now ignore the notation `+take ... = Owned<int>(p)+`. Since `+read+` maintains this ownership, we also add a corresponding postcondition, whereby `+read+` returns ownership of `+p+` after it is finished executing, in the form of another `+Owned<int>(p)+` resource.
+In this example we can ensure the safe execution of `+read+` by adding a precondition that requires ownership of `+Owned<int>(p)+`, as shown below. For now ignore the notation `+take ... = Owned<int>(p)+`. Since reading the pointer does not disturb its value, we also add a corresponding postcondition, whereby `+read+` returns ownership of `+p+` after it is finished executing, in the form of another `+Owned<int>(p)+` resource.
 
 include_example(solutions/read.c)
 
-This specifications means that
+This specification means that:
 
 * any function calling `+read+` has to be able to provide a resource `+Owned<int>(p)+` to pass into `+read+`, and
 
@@ -226,33 +278,41 @@ This specifications means that
 
 === Resource outputs
 
-However, a caller of `+read+` may also wish to know that `+read+` actually returns the correct value, the pointee of `+p+`, and also that it does not change memory at location `+p+`. To phrase both we need a way to refer to the pointee of `+p+`.
+A caller of `+read+` may also wish to know that `+read+` actually returns the correct value, the pointee of `+p+`, and also that it does not change memory at location `+p+`. To phrase both we need a way to refer to the pointee of `+p+`.
+
+// TODO: BCP: The idea that "resources have outputs" is very mind-boggling to many new users, *especially* folks with some separation logic background.  Needs to be explained very carefully.  Also, there's some semantic muddle in the terminology: Is a resource (1) a thing in the heap, (2) a thing in the heap that one is currently holding, or (3) the act of holding a thing in the heap?  These are definitely not at all the same thing, but our language at different points suggests all three!  To me, (1) is the natural sense of the word "resource"; (2) is somewhat awkward, and (3) is extremely awkward.
+
+In CN, resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned<T>(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`.
+// TODO: BCP: ... in a given heap!  (The real problem here is that "and the associated ownership" is pretty vague.)
 
-In CN resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned<T>(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`.
+CN uses the `+take+`-notation seen in the example above to bind the output of a resource to a new name. The precondition `+take P = Owned<int>(p)+` does two things: (1) it assert ownership of resource `+Owned<int>(p)+`, and (2) it binds the name `+P+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+P_post+` for the pointee value on function return.
 
-CN uses the `+take+`-notation seen in the example above to refer to the output of a resource, introducing a new name binding for the output. The precondition `+take v1 = Owned<int>(p)+` from the precondition does two things: (1) it assert ownership of resource `+Owned<int>(p)+`, and (2) it binds the name `+v1+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+v2+` for the pointee value on function return.
+// TODO: BCP: But, as we've discussed, the word "take" in the postcondition is quitre confusing: What it's doing is precisely the *opposite* of "taking" the resournce, not taking it but giving it back!!  It would be much better if we could choose a more neutral word that doesn't imply either taking or giving.  E.g. "resource".
 
-That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions: we specify
+// TODO: BCP: This might be a good place for a comment on naming conventions
 
-. that `+read+` returns `+v1+` (the initial pointee value of `+p+`), and
-. that the pointee values `+v1+` and `+v2+` before and after execution of `+read+` (respectively) are the same.
+That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions specifying
 
-include_example(solutions/read2.c)
+. that `+read+` returns `+P+` (the initial pointee value of `+p+`), and
+. that the pointee values `+P+` and `+P_post+` before and after execution of `+read+` (respectively) are the same.
 
-*Aside.* In standard separation logic the equivalent specification for `+read+` could have been phrased as follows (where `+return+` binds the return value in the postcondition):
+include_example(exercises/read2.c)
+
+*Aside.* In standard separation logic, the equivalent specification for `+read+` could have been phrased as follows (where `+\return+` binds the return value in the postcondition):
 
 ....
 ∀p.
-∀v1. { p ↦ v1 }
-     read(p)
-     { return. ∃v2. (p ↦ v2) /\ return = v1 /\ v1 = v2 }
+  ∀v1.
+    { p ↦ P }
+    read(p)
+    { \return. ∃P_post. (p ↦ P_post) /\ return = P /\ P = P_post }
 ....
 
-CN’s `+take+` notation is just alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them.
+CN’s `+take+` notation is just an alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them.
 
 === Exercises
 
-*Quadruple*. Specify the function `+quadruple_mem+`, that is similar to the earlier `+quadruple+` function, except that the input is passed as an `+int+` pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged.
+*Quadruple*. Specify the function `+quadruple_mem+`, which is similar to the earlier `+quadruple+` function, except that the input is passed as an `+int+` pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged.
 
 include_example(exercises/slf_quadruple_mem.c)
 
@@ -271,7 +331,7 @@ include_example(exercises/read.broken.c)
 CN rejects this program with the following message:
 
 ....
-cn build/exercises/read.broken.c
+cn verify exercises/read.broken.c
 [1/1]: read
 build/exercises/read.broken.c:4:3: error: Left-over unused resource 'Owned<signed int>(p)(v1)'
   return *p;
@@ -279,37 +339,71 @@ build/exercises/read.broken.c:4:3: error: Left-over unused resource 'Owned<signe
 Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_17eb4a.html
 ....
 
-CN has typechecked the function, verified that it is safe to execute under the precondition (given ownership `+Owned<int>(p)+`), and that the function (vacuously) satisfies its postcondition. But, following the check of the postcondition it finds that not all resources have been "`used up`".
-
-Given the above specification, `+read+` leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error.
+CN has typechecked the function and verified (1) that it is safe to
+execute under the precondition (given ownership `+Owned<int>(p)+`) 
+and (2) that the function (vacuously) satisfies its postcondition. But
+following the check of the postcondition it finds that not all
+resources have been "`used up`".
 
-CN’s resource types are _linear_ (as opposed to affine). This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or "`forgotten`". Every resource passed into a function has to either be used up by it, by returning it or passing it to another function that consumes it, or destroyed, by deallocating the owned area of memory (as we shall see later).
+Indeed, given the above specification, `+read+` leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error.
 
-CN’s motivation for linear tracking of resources is its focus on low-level systems software. CN checks C programs, in which, unlike higher-level garbage-collected languages, memory is managed manually, and memory leaks are typically very undesirable.
+CN’s resource types are _linear_. This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or "`forgotten`". Every resource passed into a function has to be either _returned_ to the caller or else _destroyed_ by deallocating the owned area of memory (as we shall see later).
 
-As a consequence, function specifications have to do precise "`book-keeping`" of their resource footprint, and, in particular, return any unused resources back to the caller.
+CN’s motivation for linear tracking of resources is its focus on
+low-level systems software in which memory is managed manually; in
+this context, memory leaks are typically very undesirable.  As a
+consequence, function specifications have to do precise bookkeeping of
+their resource footprint and, in particular, return any unused
+resources back to the caller.
 
 === The Block resource type
 
-Aside from the `+Owned+` resource seen so far, CN has another built-in resource type: `+Block+`. Given a C-type `+T+` and pointer `+p+`, `+Block<T>(p)+` asserts the same ownership as `+Owned<T>(p)+` — so ownership of a memory cell at `+p+` the size of type `+T+` — but in contrast to `+Owned+`, `+Block+` memory is not necessarily initialised.
+Aside from the `+Owned+` resources seen so far, CN has another
+built-in resource type called `+Block+`. Given a C-type `+T+` and
+pointer `+p+`, `+Block<T>(p)+` asserts the same ownership as
+`+Owned<T>(p)+` — ownership of a memory cell at `+p+` the size of
+type `+T+` — but, in contrast to `+Owned+`, `+Block+` memory is not
+assumed to be initialised.
 
 CN uses this distinction to prevent reads from uninitialised memory:
 
-* A read at C-type `+T+` and pointer `+p+` requires a resource `+Owned<T>(p)+`, i.e., ownership of _initialised_ memory at the right C-type. The load returns the `+Owned+` resource unchanged.
+* A read at C-type `+T+` and pointer `+p+` requires a resource
+  `+Owned<T>(p)+`, i.e., ownership of _initialised_ memory at the
+  right C-type. The load returns the `+Owned+` resource unchanged.
 
-* A write at C-type `+T+` and pointer `+p+` needs only a `+Block<T>(p)+` (so, unlike reads, writes to uninitialised memory are fine). The write consumes ownership of the `+Block+` resource (it destroys it) and returns a new resource `+Owned<T>(p)+` with the value written as the output. This means the resource returned from a write records the fact that this memory cell is now initialised and can be read from.
+* A write at C-type `+T+` and pointer `+p+` needs only a
+  `+Block<T>(p)+` (so, unlike reads, writes to uninitialised memory
+  are fine). The write consumes ownership of the `+Block+` resource
+  (it destroys it) and returns a new resource `+Owned<T>(p)+` with the
+  value written as the output. This means the resource returned from a
+  write records the fact that this memory cell is now initialised and
+  can be read from.
+// TODO: BCP: Not sure I understand "returns a new resource `+Owned<T>(p)+` with the value written as the output" -- perhaps in part because I don't understand what the output of a resource means when the resource is not in the context o a take expression.
 
-Since `+Owned+` carries the same ownership as `+Block+`, just with the additional information that the `+Owned+` memory is initalised, a resource `+Owned<T>(p)+` is "`at least as good`" as `+Block<T>(p)+` — an `+Owned<T>(p)+` resource can be used whenever `+Block<T>(p)+` is needed. For instance CN’s type checking of a write to `+p+` requires a `+Block<T>(p)+`, but if an `+Owned<T>(p)+` resource is what is available, this can be used just the same. This allows an already-initialised memory cell to be over-written again.
+Since `+Owned+` carries the same ownership as `+Block+`, just with the
+additional information that the `+Owned+` memory is initalised, a
+resource `+Owned<T>(p)+` is "`at least as good`" as `+Block<T>(p)+` —
+an `+Owned<T>(p)+` resource can be used whenever `+Block<T>(p)+` is
+needed. For instance CN’s type checking of a write to `+p+` requires a
+`+Block<T>(p)+`, but if an `+Owned<T>(p)+` resource is what is
+available, this can be used just the same. This allows an
+already-initialised memory cell to be over-written again.
 
-Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output: its output is `+void+`/`+unit+`.
+Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output.
 
-=== Write example
+=== Writing through pointers
 
-Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the pointee value.
+Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the value in the memory cell that it poinbts to.
 
-include_example(solutions/slf0_basic_incr.signed.c)
+include_example(exercises/slf0_basic_incr.signed.c)
 
-In the precondition we assert ownership of resource `+Owned<int>(p)+`, binding its output/pointee value to `+v1+`, and use `+v1+` to specify that `+p+` must point to a sufficiently small value at the start of the function not to overflow when incremented. The postcondition asserts ownership of `+p+` with output `+v2+`, as before, and uses this to express that the value `+p+` points to is incremented by `+incr+`: `+v2 == v1+1i32+`.
+In the precondition we assert ownership of resource `+Owned<int>(p)+`,
+binding its output/pointee value to `+P+`, and use `+P+` to specify
+that `+p+` must point to a sufficiently small value at the start of
+the function so as not to overflow when incremented. The postcondition
+asserts ownership of `+p+` with output `+P_post+`, as before, and uses
+this to express that the value `+p+` points to is incremented by
+`+incr+`: `+P_post == P + 1i32+`.
 
 If we incorrectly tweaked this specification and used `+Block<int>(p)+` instead of `+Owned<int>(p)+` in the precondition, as below, then CN would reject the program.
 
@@ -325,13 +419,22 @@ Resource needed: Owned<signed int>(p)
 Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_5da0f3.html
 ....
 
-The `+Owned<int>(p)+` resource required for reading is missing, since, as per precondition, only `+Block<int>(p)+` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure:
+The `+Owned<int>(p)+` resource required for reading is missing, since, per the precondition, only `+Block<int>(p)+` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure:
+
+* `+Block<signed int>(p)(u)+`, i.e., ownership of uninitialised memory
+  at location `+p+`; the output is a `+void+`/`+unit+` value `+u+`
+  (specified in the second pair of parentheses)
 
-* `+Block<signed int>(p)(u)+`, so ownership of uninitialised memory at location `+p+`; the output is a `+void+`/`+unit+` value `+u+` (specified in the second pair of parentheses)
+* `+Owned<signed int*>(&ARG0)(p)+`, the ownership of (initialised)
+  memory at location `+&ARG0+`, i.e., the memory location where the
+  first function argument is stored; its output is the pointer `+p+`
+  (not to be confused with the pointee of `+p+`); and finally
 
-* `+Owned<signed int*>(&ARG0)(p)+`, the ownership of (initialised) memory at location `+&ARG0+`, so the memory location where the first function argument is stored; its output is the pointer `+p+` (not to be confused with the pointee of `+p+`); and finally
+* `+__CN_Alloc(&ARG0)(void)+` is a resource that records allocation
+  information for location `+&ARG0+`; this is related to CN’s
+  memory-object semantics, which we ignore for the moment.
 
-* `+__CN_Alloc(&ARG0)(void)+` is a resource that records allocation information for location `+&ARG0+`; this is related to CN’s memory-object semantics, which we ignore for the moment.
+// TODO: BCP: These bullet points are all a bit mysterious and maybe TMI.  More generally, we should double check that this is actually the information displayed in the current HTML output...
 
 === Exercises
 
@@ -345,17 +448,28 @@ include_example(exercises/slf3_basic_inplace_double.c)
 
 === Multiple owned pointers
 
-When functions manipulate multiple pointers, we can assert their ownership just like before. However (as in standard separation logic) pointer ownership is unique, so simultaneous ownership of `+Owned+` or `+Block+` resources for two pointers requires these pointers to be disjoint.
+When functions manipulate multiple pointers, we can assert their
+ownership just like before. However 
+pointer ownership in CN is unique -- that is, simultaneously owning
+`+Owned+` or `+Block+` resources for two pointers implies that these
+pointers are disjoint.
 
-The following example shows the use of two `+Owned+` resources for accessing two different pointers: function `+add+` reads two `+int+` values in memory, at locations `+p+` and `+q+`, and returns their sum.
+The following example shows the use of two `+Owned+` resources for
+accessing two different pointers by a function `+add+`, which reads
+two `+int+` values in memory, at locations `+p+` and `+q+`, and
+returns their sum.
+
+// TODO: BCP: Hmmm -- I'm not very sure that the way I've been naming things is actually working that well.  The problem is that in examples like this we computer "thing pointed to by p" at both C and CN levels.  At the C level, the thing pointed to by p obviously cannot also be called p, so it doesn't make sense for it to be called P at the CN level, right?  Maybe we need to think again, but hoinestly I am not certain that it is *not* working either.  So I'm going to opush on for now...
 
 include_example(exercises/add_read.c)
 
 This time we use C’s `+unsigned int+` type. In C, over- and underflow of unsigned integers is not undefined behaviour, so we do not need any special preconditions to rule this out. Instead, when an arithmetic operation at unsigned type goes outside the representable range, the value "`wraps around`".
 
-The CN variables `+m+` and `+n+` (resp. `+m2+` and `+n2+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type.
+The CN variables `+P+` and `+Q+` (resp. `+P_post+` and `+Q_post+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type.
+
+Hence, the postcondition `+return == P + Q+` holds also when the sum of `+P+` and `+Q+` is greater than the maximal `+unsigned int+` value.
 
-Hence, the postcondition `+return == m+n+` holds also when the sum of `+m+` and `+n+` is greater than the maximal `+unsigned int+` value.
+// TODO: BCP: I wonder whether we should uniformly use i32 integers everywhere in the tutorial (just mentioning in the bullet list below that there are other integer types, and using i64 for calculations that may overflow).  Forgetting which integer type I was using was a common (and silly) failure mode when I was first working through the tutorial.
 
 In the following we will sometimes use unsigned integer types to focus on specifying memory ownership, rather than the conditions necessary to show absence of C arithmetic undefined behaviour.
 
@@ -371,23 +485,30 @@ include_example(exercises/slf8_basic_transfer.c)
 
 == Ownership of compound objects
 
-So far all examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types.
+So far, our examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types.
 
 For instance, the following example uses a `+struct+` `+point+` to represent a point in two-dimensional space. The function `+transpose+` swaps a point’s `+x+` and `+y+` coordinates.
 
 include_example(exercises/transpose.c)
 
-Here the precondition asserts ownership for `+p+`, at type `+struct point+`; the output `+s+` is a value of CN type `+struct point+`, i.e. a record with members `+i32+` `+x+` and `+i32+` `+y+`. The postcondition similarly asserts ownership of `+p+`, with output `+s2+`, and asserts the coordinates have been swapped, by referring to the members of `+s+` and `+s2+` individually.
+Here the precondition asserts ownership for `+p+`, at type `+struct
+point+`; the output `+P_post+` is a value of CN type `+struct point+`,
+i.e. a record with members `+i32+` `+x+` and `+i32+` `+y+`. The
+postcondition similarly asserts ownership of `+p+`, with output
+`+P_post+`, and asserts the coordinates have been swapped, by referring to
+the members of `+P+` and `+P_post+` individually.
+
+// TODO: BCP: This paragraph is quite confusing if read carefully: it seems to say that the "take" in the requires clause returns a different type than the "tajke" in the "ensures" clause.  Moreover, even if the reader decides that this cannot be the case and they have to return the same type, they may wonder whether thius type is a C type (which is what it looks like, since there is only one struct declaration, and it is not in a magic comment) or a CN type (which might be expected, since it is the result of a "take").  I *guess* what's going on here is that every C type is automatically reflected as a CN type with the same name.  But this story is also not 100% satisfying, since the basic numeric types don't work this way: each C numeric type has an *analog* in CN, but with a different name.  
 
 === Compound Owned and Block resources
 
-While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and pass these as values, even to other functions.
+While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and manipulate these as values, including even passing them to other functions.
 
-CN therefore cannot treat resources for compound C types, such as structs, as primitive, indivisible units. Instead, `+Owned<T>+` and `+Block<T>+` are defined inductively in the structure of the C-type `+T+`.
+CN therefore cannot treat resources for compound C types like structs as primitive, indivisible units. Instead, `+Owned<T>+` and `+Block<T>+` are defined inductively on the structure of the C-type `+T+`.
 
-For struct types `+T+`, the `+Owned<T>+` resource is defined as the collection of `+Owned+` resources for its members (as well as `+Block+` resources for any padding bytes in-between). The resource `+Block<T>+`, similarly, is made up of `+Block+` resources for all members (and padding bytes).
+For struct types `+T+`, the `+Owned<T>+` resource is defined as the collection of `+Owned+` resources for its members (as well as `+Block+` resources for any padding bytes in-between them). The resource `+Block<T>+`, similarly, is made up of `+Block+` resources for all members (and padding bytes).
 
-To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and recompose it, as needed. The following example illustrates this.
+To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and it can recompose the struct later, as needed. The following example illustrates this.
 
 Recall the function `+zero+` from our earlier exercise. It takes an `+int+` pointer to uninitialised memory, with `+Block<int>+` ownership, and initialises the value to zero, returning an `+Owned<int>+` resource with output `+0+`.
 
@@ -397,25 +518,29 @@ include_example(exercises/init_point.c)
 
 As stated in its precondition, `+init_point+` receives ownership `+Block<struct point>(p)+`. The `+zero+` function, however, works on `+int+` pointers and requires `+Block<int>+` ownership.
 
-CN can prove the calls to `+zero+` with `+&p->x+` and `+&p->y+` are safe because it decomposes the `+Block<struct point>(p)+` into two `+Block<int>+`, one for member `+x+`, one for member `+y+`. Later, the reverse happens: following the two calls to `+zero+`, as per `+zero+`’s precondition, `+init_point+` has ownership of two adjacent `+Owned<int>+` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `+init_point+` requires ownership `+Owned<struct point>(p)+`, CN combines these back into a compound resource. The resulting `+Owned<point struct>+` resource has for an output the struct value `+s2+` that is composed of the zeroed member values for `+x+` and `+y+`.
+CN can prove the calls to `+zero+` with `+&p->x+` and `+&p->y+` are safe because it decomposes the `+Block<struct point>(p)+` into a `+Block<int>+` for member `+x+` and a `+Block<int>+` for member `+y+`. Later, the reverse happens: following the two calls to `+zero+`, as per `+zero+`’s precondition, `+init_point+` has ownership of two adjacent `+Owned<int>+` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `+init_point+` requires ownership `+Owned<struct point>(p)+`, CN combines these back into a compound resource. The resulting `+Owned<point struct>+` resource has for an output the struct value `+P_post+` that is composed of the zeroed member values for `+x+` and `+y+`.
 
 === Resource inference
 
 To handle the required resource inference, CN "`eagerly`" decomposes all `+struct+` resources into resources for the struct members, and "`lazily`" re-composes them as needed.
 
-We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function (more on CN assertions later), so we can inspect CN’s proof context shown in the error report.
+We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function, so we can inspect CN’s proof context shown in the error report.  (More on CN assertions later.)
+
+// TODO: BCP: Recheck that what we say here matches what it actually looks like
 
 include_example(exercises/transpose.broken.c)
 
 The precondition of `+transpose+` asserts ownership of an `+Owned<struct point>(p)+` resource. The error report now instead lists under "`Available resources`" two resources:
 
-* `+Owned<signed int>(member_shift<point>(p, x))+` with output `+s.x+` and
+* `+Owned<signed int>(member_shift<point>(p, x))+` with output `+P.x+` and
+
+* `+Owned<signed int>(member_shift<point>(p, y))+` with output `+P.y+`
 
-* `+Owned<signed int>(member_shift<point>(p, y))+` with output `+s.y+`
+// TODO: BCP: We should verify that it really does say this.
 
 Here `+member_shift<s>(p,m)+` is the CN expression that constructs, from a `+struct s+` pointer `+p+`, the "`shifted`" pointer for its member `+m+`.
 
-When the function returns the two member resources are recombined "`on demand`" to satisfy the postcondition `+Owned<struct point>(p)+`.
+When the function returns, the two member resources are recombined "`on demand`" to satisfy the postcondition `+Owned<struct point>(p)+`.
 
 === Exercises
 
@@ -437,9 +562,11 @@ CP: Agreed. For now continuing with arrays, but will return to this later.
 
 == Arrays and loops
 
-Another common datatype in C is arrays. Reasoning about memory ownership for arrays is more difficult than for the datatypes we have seen so far: C allows the programmer to access arrays using _computed pointers_, and the size of an array does not need to be known as a constant at compile time.
+Another common datatype in C is arrays. Reasoning about memory ownership for arrays is more difficult than for the datatypes we have seen so far, for two reasons: (1) C allows the programmer to access arrays using _computed pointers_, and (2) the size of an array does not need to be known as a constant at compile time.
 
-To support reasoning about code manipulating arrays and computed pointers, CN has _iterated resources_. For instance, to specify ownership of an `+int+` array with 10 cells starting at pointer `+p+`, CN uses the iterated resource
+To support reasoning about code manipulating arrays and computed pointers, CN has _iterated resources_. For instance, to specify ownership of an `+int+` array with 10 cells starting at pointer `+p+`, CN uses the following iterated resource:
+
+// TODO: BCP: Another tricky naming / capitalization puzzle: The index of an "each" has CN type i32, so strictly speaking I believe it should be written with a capital "I".  But insisting on this feels like insisting on a distinction that most CN programmers would never even notice, much less be confused by.  I think this is another instance of the way C and CN integer types are partly but not completely squished together.
 
 [source,c]
 ----
@@ -476,7 +603,7 @@ comprising three parts:
 
 === First array example
 
-Let’s see how this applies to a first example of an array-manipulating function. Function `+read+` takes three arguments: the base pointer `+p+` of an `+int+` array, the length `+n+` of the array, and an index `+i+` into the array; `+read+` then returns the value of the `+i+`-th array cell.
+Let’s see how this applies to a simple array-manipulating function. Function `+read+` takes three arguments: the base pointer `+p+` of an `+int+` array, the length `+n+` of the array, and an index `+i+` into the array; `+read+` then returns the value of the `+i+`-th array cell.
 
 include_example(exercises/array_load.broken.c)
 
@@ -490,7 +617,7 @@ On exit the array ownership is returned again.
 This specification, in principle, should ensure that the access `+p[i]+` is safe. However, running CN on the example produces an error: CN is unable to find the required ownership for reading `+p[i]+`.
 
 ....
-cn build/solutions/array_load.broken.c
+cn verify solutions/array_load.broken.c
 [1/1]: read
 build/solutions/array_load.broken.c:5:10: error: Missing resource for reading
   return p[i];
@@ -498,13 +625,13 @@ build/solutions/array_load.broken.c:5:10: error: Missing resource for reading
 Resource needed: Owned<signed int>(array_shift<signed int>(p, (u64)i))
 ....
 
-The reason is that when searching for a required resource, such as the `+Owned+` resource for `+p[i]+` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user.
+The reason is that, when searching for a required resource, such as the `+Owned+` resource for `+p[i]+` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user.
 
-To make the `+Owned+` resource required for accessing `+p[i]+` available to CN’s resource inference we have to "`extract`" ownership for index `+i+` out of the iterated resource.
+To make the `+Owned+` resource required for accessing `+p[i]+` available to CN’s resource inference we have to explicitly "`extract`" ownership for index `+i+` out of the iterated resource.
 
 include_example(exercises/array_load.c)
 
-Here the CN comment `+/*@ extract Owned<int>, i; @*/+` is a CN "`ghost statement`"/proof hint that instructs CN to instantiate any available iterated `+Owned<int>+` resource for index `+i+`. In our example this operation splits the iterated resource into two:
+Here the CN comment `+/*@ extract Owned<int>, i; @*/+` is a proof hint in the form of a "`ghost statement`" that instructs CN to instantiate any available iterated `+Owned<int>+` resource for index `+i+`. In our example this operation splits the iterated resource into two:
 
 [source,c]
 ----
@@ -529,21 +656,34 @@ each(i32 j; 0i32 <= j && j < n && j != i)
 
 After this extraction step, CN can use the (former) extracted resource to justify the access `+p[i]+`.
 
-Following an `+extract+` statement, CN moreover remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function.
+Following an `+extract+` statement, CN remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function.
 
-So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+i32+` and the iterated resource is `+Owned<int>+`, the output `+a1+` is a map from `+i32+` indices to `+i32+` values — CN type `+map<i32,i32>+`. (If the type of `+j+` was `+i64+` and the resource `+Owned<char>+`, `+a1+` would have type `+map<i64,u8>+`.)
+So far the specification only guarantees safe execution but does not
+specify the behaviour of `+read+`. To address this, let’s return to
+the iterated resources in the function specification. When we specify
+`+take A = each ...+` here, what is `+A+`? In CN, the output of an
+iterated resource is a _map_ from indices to resource outputs. In this
+example, where index `+j+` has CN type `+i32+` and the iterated
+resource is `+Owned<int>+`, the output `+A+` is a map from `+i32+`
+indices to `+i32+` values — CN type `+map<i32,i32>+`. If the type of
+`+j+` was `+i64+` and the resource `+Owned<char>+`, `+A+` would have
+type `+map<i64,u8>+`.
 
 We can use this to refine our specification with information about the functional behaviour of `+read+`.
 
 include_example(exercises/array_load2.c)
 
-We specify that `+read+` does not change the array — the outputs `+a1+` and `+a2+`, taken before and after running the function, are the same — and that the value returned is `+a1[i]+`, `+a1+` at index `+i+`.
+We specify that `+read+` does not change the array — the outputs of `+Owned+`, 
+`+A+` and `+A_post+`, taken before and after running the function, are
+the same — and that the value returned is `+A[i]+`.
 
 === Exercises
 
 
 *Array read two.* Specify and verify the following function, `+array_read_two+`, which takes the base pointer `+p+` of an `+unsigned int+` array, the array length `+n+`, and two indices `+i+` and `+j+`. Assuming `+i+` and `+j+` are different, it returns the sum of the values at these two indices.
 
+// TODO: BCP: When we get around to renaming files in the examples directory, we should call this one array_swap or something else beginning with "array".
+
 include_example(exercises/add_two_array.c)
 
 ////
@@ -578,15 +718,17 @@ TODO: BCP: I wrote this, which seemed natural but did not work -- I still don't
 
 === Loops
 
-The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to *loop*, uniformly accessing all cells of an array, or sub-ranges of it.
+The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to *loop*, uniformly accessing all cells of an array or a sub-range of it.
 
 In order to verify code with loops, CN requires the user to supply loop invariants -- CN specifications of all owned resources and the constraints required to verify each iteration of the loop.
 
-
 Let's take a look at a simple first example. The following function, `+init_array+`, takes the base pointer `+p+` of a `+char+` array and the array length `+n+` and writes `+0+` to each array cell.
+
+// TODO: BCP: Rename to array_init.c
+
 include_example(exercises/init_array.c)
 
-If, for the moment, we focus just on proving safe execution of `+init_array+`, ignoring its functional behaviour, a specification might look as above: on entry `+init_array+` takes ownership of an iterated `+Owned<char>+` resource -- one `+Owned+` resource for each index `+i+` of type `+u32+` (so necessarily greater or equal to `+0+`) up to `+n+`; on exit `+init_array+` returns the ownership.
+If, for the moment, we focus just on proving safe execution of `+init_array+`, ignoring its functional behaviour, a specification might look as above: on entry, `+init_array+` takes ownership of an iterated `+Owned<char>+` resource -- one `+Owned+` resource for each index `+i+` of type `+u32+` (so necessarily greater or equal to `+0+`) up to `+n+`; on exit `+init_array+` returns the ownership.
 
 To verify this, we have to supply a loop invariant that specifies all resource ownership and the necessary constraints that hold before and after each iteration of the loop. Loop invariants are specified using the keyword `inv`, followed by CN specifications using the same syntax as in function pre- and postconditions. The variables in scope for loop invariants are all in-scope C variables, as well as CN variables introduced in the function precondition. *In loop invariants, the name of a C variable refers to its current value* (more on this shortly).
 
@@ -597,7 +739,7 @@ TODO: BCP: Concrete syntax: Why not write something like "unchanged {p,n}" or "u
 
 The main condition here is unsurprising: we specify ownership of an iterated resource for an array just like in the the pre- and postcondition.
 
-The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable, and so CN permits this as well.While in this example it is obvious that `+p+` and `+n+` do not change, CN currently requires the loop invariant to explicitly state this, using special notation `+{p} unchanged+` (and similarly for `+n+`).
+The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable. Although, in this example, it is obvious that `+p+` and `+n+` do not change, CN currently requires the loop invariant to explicitly state this, using special notation `+{p} unchanged+` (and similarly for `+n+`).
 
 **Note.** If we forget to specify `+unchanged+`, this can lead to confusing errors. In this example, for instance, CN would verify the loop against the loop invariant, but would be unable to prove a function postcondition seemingly directly implied by the loop invariant (lacking the information that the postcondition's `+p+` and `+n+` are the same as the loop invariant's). Future CN versions may handle loop invariants differently and treat variables as immutable by default.
 ////
@@ -607,19 +749,23 @@ TODO: BCP: This seems like a good idea!
 The final piece needed in the verification is an `+extract+` statement, as used in the previous examples: to separate the individual `+Owned<char>+` resource for index `+j+` out of the iterated `+Owned+` resource and make it available to the resource inference, we specify `+extract Owned<char>, j;+`.
 
 
-With the `+extract+` statements in place, CN accepts the function.
+With the `+inv+` and `+extract+` statements in place, CN accepts the function.
 
 === Second loop example
 
-However, on closer look, the specification of `+init_array+` is overly strong: it requires an iterated `+Owned+` resource for the array on entry. If, as the name suggests, the purpose of `+init_array+` is to initialise the array, then a precondition asserting only an iterated `+Block+` resource for the array should also be sufficient. The modified specification is then as follows.
+The specification of `+init_array+` is overly strong: it requires an iterated `+Owned+` resource for the array on entry. If, as the name suggests, the purpose of `+init_array+` is to initialise the array, then a precondition asserting only an iterated `+Block+` resource for the array should also be sufficient. The modified specification is then as follows.
 
 include_example(exercises/init_array2.c)
 
-This specification *should* hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `+Block+` to `+Owned+` "`state`", so that on function return the full array is initialised. (Recall that stores only require `+Block+` ownership of the written memory location, so ownership of not-necessarily-initialised memory.)
+This specification *should* hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `+Block+` to `+Owned+` "`state`", so that on function return the full array is initialised. (Recall that stores only require `+Block+` ownership of the written memory location, i.e., ownership of not-necessarily-initialised memory.)
 
-To verify this modified example we again need a loop invariant. This time, the loop invariant is more involved, however: since each iteration of the loop initialises one more array cell, the loop invariant has to do precise book-keeping of the initialisation status of the array.
+To verify this modified example we again need a loop Invariant. But
+this time the loop invariant is more involved: since each iteration of
+the loop initialises one more array cell, the loop invariant has to do
+precise book-keeping of the initialisation status of the different
+sections of the array.
 
-To do so, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `+Owned+` resource, for all other array indices we have the (unchanged) `+Block+` ownership.
+To do this, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `+Owned+` resource, for all other array indices we have the (unchanged) `+Block+` ownership.
 
 include_example(solutions/init_array2.c)
 
@@ -631,16 +777,17 @@ Let's go through this line-by-line:
 
 - As in the previous example, we assert `+p+` and `+n+` are unchanged.
 
-- Finally, unlike in the previous example, this loop invariant involves `+j+`. We therefore also need to know that `+j+` does not exceed the array length `+n+`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `+j=n+` holds. This, in turn, is needed to show that when the function returns, ownership of the iterated `+Owned+` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource.
+- Finally, unlike in the previous example, this loop invariant involves `+j+`. We therefore also need to know that `+j+` does not exceed the array length `+n+`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `+j=n+` holds. This, in turn, is needed to show that, when the function returns, ownership of the iterated `+Owned+` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource.
 
 As before, we also have to instruct CN to `+extract+` ownership of individual array cells out of the iterated resources:
 
-- to allow CN to extract the individual `+Block+` to be written we use `+extract Block<char>, j;+`;
+- to allow CN to extract the individual `+Block+` to be written, we use `+extract Block<char>, j;+`;
 
 - the store returns a matching `+Owned<char>+` resource for index `+j+`;
 
-- finally, we put `+extract Owned<char>, j;+` to allow CN to "`attach`" this resource to the iterated `+Owned+` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `+extract+` only for the "`reverse`" direction.
+- finally, we add `+extract Owned<char>, j;+` to allow CN to "`attach`" this resource to the iterated `+Owned+` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `+extract+` only for the "`reverse`" direction.
 
+// TODO: BCP: That last bit is mysterious.
 
 === Exercises
 
@@ -648,7 +795,7 @@ As before, we also have to instruct CN to `+extract+` ownership of individual ar
 
 include_example(exercises/init_array_rev.c)
 
-
+// TODO: BCP: The transition to the next section is awkward.  Needs a sentence or two to signal that we're changing topics.  Some better visual indication would also be nice.
 
 ////
 ___________________________________________________________________________
@@ -679,17 +826,27 @@ not alias...
 include_example(exercises/slf_incr2_noalias.c)
 
 But what if they do alias?  The clunky solution is to write a whole
-different version of incr2 with a different embedded specification...
+different version of `+incr2+` with a different embedded specification...
 
 include_example(exercises/slf_incr2_alias.c)
 
-This is horrible.  Much better is to define a predicate to use
-in the pre- and postconditions that captures both cases together:
+This version does correctly state that the final values of `+p+` and `+q+` are,m respectively, `+3+` and `+1+` more than their original values.  But the way we got there -- by duplicating the whole function `+incr2+`, is horrible.
+
+A better way is to define a *predicate* that captures both the aliased
+and the non-aliased cases together and use it in the pre- and
+postconditions:
 
 include_example(exercises/slf_incr2.c)
 
+// TODO: BCP: "BothOwned" is a pretty awkward name.
+// TODO: BCP: We haven't introduced CN records.  In particular, C programmers may be surprised that we don't have to pre-declare record types.
+// TODO: BCP: the annotation on incr2 needs some unpacking for readers!!
+// TODO: BCP: first use of the "split_case" annotation
+
 == Allocating and Deallocating Memory
 
+// TODO: BCP: Again, more text is needed to set up this discussion.
+
 At the moment, CN does not understand the `+malloc+` and `+free+`
 functions.  They are a bit tricky because they rely on a bit of
 polymorphism and a typecast between `+char*+` -- the result type of
@@ -700,7 +857,7 @@ However, for any given type, we can define a type-specific function
 that allocates heap storage with exactly that type.  The
 implementation of this function cannot be checked by CN, but we can
 give just the spec, together with a promise to link against an
-external C library providing the implementation:
+external C library providing a correct (but not verified!) implementation:
 
 include_example(exercises/malloc.h)
 
@@ -709,9 +866,11 @@ inside a CN file by marking it with the keyword `+trusted+` at the top
 of its CN specification.)
 
 Similarly:
+
 include_example(exercises/free.h)
 
 Now we can write code that allocates and frees memory:
+
 include_example(exercises/slf17_get_and_free.c)
 
 We can also define a "safer", ML-style version of `+malloc+` that
@@ -735,51 +894,57 @@ pointed to by its argument.
 
 include_example(exercises/slf_ref_greater.c)
 
-=== Side Note
+=== Side note
 
 Here is another syntax for external / unknown
 functions, together with an example of a loose specification:
 
 ////
-TODO: BCP: This is a bit random -- it's not clear people need to know about this alternate syntax, and it's awkwardly mixed with a semi-interesting example that's not relevant to this section.
+TODO: BCP: This is a bit random -- it's not clear people need to know about this alternate syntax, and it's awkwardly mixed with a semi-interesting example that's not relevant to this section.  Also awkwardly placed, right here.
 ////
 
 include_example(exercises/slf18_two_dice.c)
 
 == Lists
 
+// TODO: BCP: Better intro needed
+
 Now it's time to look at some more interesting heap structures.
 
 To begin with, here is a C definition for linked list cells, together
 with allocation and deallocation functions:
 
+// TODO: BCP: Here and in several other places, we should use the "take _ = ..." syntax when the owned value is not used.  And we should explain it the first time we use it.
+
 include_example(exercises/list_c_types.h)
 
+// TODO: BCP: Per discussion with Christopher, Cassia, and Daniel, the word "predicate" is quite confusing for newcomers (in logic, predicates do not return things!).  A more neutral word might make for significantly easier onboarding.
+
 To write specifications for C functions that manipulate lists, we need
-to define a CN "predicate" that describes *mathematical* list
-structures, as one would do in ML, Haskell, or Coq.  (We call them
-"sequences" here to avoid overloading the word "list".)
+to define a CN "predicate" that describes specification-level list
+structures, as one would do in ML, Haskell, or Coq.  We use the
+datatype `+List+` for CN-level lists.
 
-Intuitively, the `+IntList+` predicate walks over a pointer structure
-in the C heap and extracts an `+Owned+` version of the mathematical
-list that it represents.
+Intuitively, the `+SLList+` predicate walks over a singly-linked
+pointer structure in the C heap and extracts an `+Owned+` version of
+the CN-level list that it represents.
 
 include_example(exercises/list_cn_types.h)
 
-We can also write specification-level "functions" by ordinary
-functional programming (in slightly strange, unholy-union-of-C-and-ML
+We can also write *functions* on CN-level lists by ordinary functional
+programming (in a slightly strange, unholy-union-of-C-and-Rust
 syntax):
 
 include_example(exercises/list_hdtl.h)
 
-We use the `+IntList+` predicate to specify functions returning the
+We use the `+SLList+` predicate to specify functions returning the
 empty list and the cons of a number and a list.
 
 include_example(exercises/list_constructors.h)
 
-Finally, we can collect all this stuff into a single header file and
+Finally, we can collect all this stuff into a single header file.  (We
 add the usual C `+#ifndef+` gorp to avoid complaints from the compiler
-if it happens to get included twice from the same source file later.
+if it happens to get included twice from the same source file later.)
 
 include_example(exercises/list.h)
 
@@ -823,6 +988,10 @@ avoids allocating any new list cells in the splitting step by taking
 alternate cells from the original list and linking them together into
 two new lists of roughly equal lengths.
 
+// TODO: BCP: We've heard from more than one reader that this example is particularly hard to digest without some additional help
+
+// TODO: BCP: Nit: Merge multiple requires and ensures clauses into one
+
 include_example(exercises/mergesort.c)
 
 === Exercises
@@ -854,7 +1023,7 @@ include_example(exercises/slf_length_acc.c)
 
 == Working with External Lemmas
 
-**TODO**: This section should also show what the proof of the lemmas
+// TODO: BCP: This section should also show what the proof of the lemmas
 looks like on the Coq side!
 
 // TODO: BCP: This needs to be filled in urgently!!
@@ -898,6 +1067,10 @@ include_example(exercises/list_rev_alt.c)
 
 **Sized stacks:** Fill in annotations where requested:
 
+// TODO: BCP: type_synonym has not been introduced yet
+
+// TODO: Mention the pun here: SizedStack is both a predicate and the type that that predicate returns.  There's no ambiguity because the latter takes no argument.
+
 include_example(exercises/slf_sized_stack.c)
 
 // ======================================================================
@@ -914,6 +1087,8 @@ include_example(exercises/slf_sized_stack.c)
 
 == CN Style
 
+// TODO: BCP: If we are agreed on the naming conventions suggested in /NAMING-CONVENTIONS.md, we could move that material here.
+
 This section gathers some advice on stylistic conventions and best
 practices in CN.
 
@@ -974,7 +1149,7 @@ element, which is the first in a linked list of `+int_queueCell+`s,
 the other pointing directly to the last cell in this list.  If the
 queue is empty, both pointers are NULL.
 
-Abstractly, a queue just represents a list, so we can reuse the `+seq+`
+Abstractly, a queue just represents a list, so we can reuse the `+List+`
 type from the list examples earlier in the tutorial.
 
 include_example(exercises/queue_cn_types_1.h)
@@ -986,12 +1161,13 @@ we have to rename other things above for consistency...
 Given a pointer to an `+int_queue+` struct, this predicate grabs
 ownership of the struct, asserts that the `+front+` and `+back+` pointers
 must either both be NULL or both be non-NULL, and then hands off to an
-auxiliary predicate `+IntQueueFB+`.  (Conceptually, `+IntQueueFB+` is
-part of `+IntQueuePTR+`, but CN currently allows conditional
-expressions only at the beginning of predicate definitions, not after
-a `+take+`.)
+auxiliary predicate `+IntQueueFB+`.  
 
-`+IntQueueFB+` is where the interesting part starts:
+`+IntQueueFB+` is where the interesting part starts.  (Conceptually,
+`+IntQueueFB+` is part of `+IntQueuePTR+`, but CN currently allows
+conditional expressions only at the beginning of predicate
+definitions, not after a `+take+`, so we need to make a separate
+auxiliary predicate.)
 
 include_example(exercises/queue_cn_types_2.h)
 
@@ -1011,7 +1187,7 @@ the second to last cell (or the `+front+` pointer, if there is only
 one cell in the list), so we need to be careful not to `+take+` this
 cell twice.
 
-Accordingly, we begin by `+take+`ing the tail cell and passing it
+Accordingly, we begin by `+take+`-ing the tail cell and passing it
 separately to the `+IntQueueAux+` predicate, which has the job of
 walking down the cells from the front and gathering all the rest of
 them into a sequence.  We take the result from `+IntQueueAux+` and
@@ -1069,7 +1245,7 @@ include_example(exercises/queue_push_orig.broken.c)
 *Exercise*: Before reading on, see if you can write down a reasonable
 top-level specification for this operation.
 
-(One thing you might find odd about this code is that there's a
+One thing you might find odd about this code is that there's a
 `+return+` statement at the end of each branch of the conditional,
 rather than a single `+return+` at the bottom.  The reason for this is
 that, when CN analyzes a function body containing a conditional, it
@@ -1078,7 +1254,7 @@ the branches.  Then, if verification encounters an error related to
 this code -- e.g., "you didn't establish the `+ensures+` conditions at
 the point of returning -- the error message will be confusing because
 it will not be clear which branch of the conditional it is associated
-with.)
+with.
 
 Now, here is the annotated version of the `+push+` operation.
 
@@ -1093,6 +1269,8 @@ elements, so we should expect that validating `+push+` is going to
 require some reasoning about this sequence.  Here, in fact, is the
 lemma we need.
 
+// TODO: BCP: Not sure I can explain what "pointer" means here, or why we don't need to declare more specific types for these arguments to the lemma.
+
 include_example(exercises/queue_push_lemma.h)
 
 This says, in effect, that we have two choices for how to read out the
@@ -1148,7 +1326,7 @@ cannot.)
 The guard/condition for `+IntQueueFB+` is `+is_null(front)+`, which is
 why we need to do a `+split_case+` on this value. On one branch of the
 `+split_case+`, we have a contradiction: the fact that `+before ==
-Seq_Nil{}+` (from `+IntQueueFB+`) conflicts with `+before != Seq_Nil+`
+Nil{}+` (from `+IntQueueFB+`) conflicts with `+before != Nil+`
 from the precondition, so that case is immediate.  On the other
 branch, CN now knows that the queue is non-empty as required and type
 checking proceeds.
@@ -1207,8 +1385,7 @@ telltale clues in the error report that suggest what the problem was?
 not `+f == b+` to find out whether we have reached the last element of
 the queue.  Another way to get the same information would be to test
 whether `+f->next == 0+`.  Can you verify this version?
-
-Note: I (BCP) have not worked out the details, so am not sure how hard
+*Note*: I (BCP) have not worked out the details, so am not sure how hard
 this is (or if it is even not possible, though I'd be surprised).
 Please let me know if you get it working!
 
@@ -1224,11 +1401,13 @@ Can you generalize the `+snoc_facts+` lemma to handle both cases?  You
 can get past the dereference with a `+split_case+` but formulating the
 lemma before the `+return+` will be a bit more complicated.
 
-Note: Again, this has not been shown to be possible, but Dhruv
+*Note*: Again, this has not been shown to be possible, but Dhruv
 believes it should be!
 
 === Doubly Linked Lists
 
+// TODO: BCP: The rest of the tutorial (from here to the end) needs to be checked for consistency of naming and capitalization conventions.
+
 A doubly linked list is a linked list where each node has a pointer
 to both the next node and the previous node. This allows for O(1)
 operations for adding or removing nodes anywhere in the list. Here is
@@ -1241,7 +1420,7 @@ track of the front or back, but rather we take any node in the list
 and have a sequence to the left and to the right of that node. The `left` 
 and `right` are from the point of view of the node itself, so `left` 
 is kept in reverse order. Additionally, similarly to in the 
-`Imperative Queues` example, we can reuse the `+seq+` type.
+`Imperative Queues` example, we can reuse the `+List+` type.
 
 include_example(exercises/Dbl_Linked_List/cn_types.h)
 
@@ -1314,8 +1493,8 @@ include_example(exercises/Dbl_Linked_List/add.c)
 First, let's look at the pre and post conditions. The `requires` 
 clause is straightforward. We need to own the list centered around 
 the node that `n` points to. `Before` is a `Dll`
-that is either empty, or it has a seq to the left,
-the current node that `n` points to, and a seq to the right.
+that is either empty, or it has a List to the left,
+the current node that `n` points to, and a List to the right.
 This corresponds to the state of the list when it is passed in.
 
 In the ensures clause, we again establish ownership of the list, but this time it is centered around the added node. This means that `After` is a `Dll` structure similar to `Before`, except that the node `curr` is 
@@ -1365,7 +1544,7 @@ Now, let's look at the annotations in the function body. These are similar to in
 
 // ======================================================================
 
-*Exercise*: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing these functions and writing their specifications.
+*Exercise*: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing a few of these functions and writing their specifications.
 
 === The Runway
 
@@ -1460,15 +1639,15 @@ Misc things to do:
 
   - naming issues
         - rename == to ptr_eq everywhere in specs
-        - rename list to seq in filenames.  or go more radical and rename seq to cnlist
-        - consider renaming IntList to just List (and int_list to just list,
+        - rename list to List in filenames.  or go more radical and rename List to cnlist
+        - consider renaming SLList to just List (and sllist to just list,
           etc.) everywhere (since we are only dealing with one kind of list
           in the tutorial, the extra pedantry is not getting us much; and
           this simplification would avoid trying to fix conventions that all
           CN code should use everywhere...)
-       - related: the name Seq_Cons is awkward for several reasons:
+       - related: the name Cons is awkward for several reasons:
            - long / verbose (nothing to do about that, I guess)
-           - Seq is capitalized, but it means seq
+           - Seq is capitalized, but it means List
            - most important part is buried in the middle
            - What are the established C conventions here??