+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:
+
+ [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:
+
+ 3 succ 0
+
+with the appropriate lambda terms substituted throughout? Since 3 is `\f z. f (f (f z))`, it should reduce to whatever:
+
+ succ (succ (succ 0))
+
+does. And if we define `succ` properly, we should expect that to give us the same lambda term that we used to encode `3` in the first place.
+
+