-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: