Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.
-We saw that using the `cons` operation and `[]` as arguments to `fold_right` over a list gave us back that very same list. In the Lambda Calculus, that would come down to:
+We saw that using the `cons` operation (Kapulet's `&`) and `[]` as arguments to `fold_right` over a list give us back that very same list. In the Lambda Calculus, that comes to the following:
[a, b, c] cons []
-with the appropriate lambda terms substituted throughout, would just reduce to the same lambda term we used to encode `[a, b, c]`. What do you think this would reduce to:
+with the appropriate lambda terms substituted throughout, just reduces to the same lambda term we used to encode `[a, b, c]`.
+
+In the same spirit, what do you expect this will reduce to:
3 succ 0
-with the appropriate lambda terms substituted throughout? Since 3 is `\f z. f (f (f z))`, it should reduce to whatever:
+Since 3 is `\f z. f (f (f z))`, it should reduce to whatever:
succ (succ (succ 0))