--- a/src/InductiveTypes.v	Mon Oct 08 16:04:49 2012 -0400
+++ b/src/InductiveTypes.v	Sun Oct 14 11:50:28 2012 -0400
@@ -780,7 +780,11 @@
   end.
 
 Definition plus_rec : nat -> nat -> nat :=
-  nat_rec (fun _ : nat => nat -> nat) (fun _ => O) (fun _ r m => S (r m)).
+  nat_rec (fun _ : nat => nat -> nat) (fun m => m) (fun _ r m => S (r m)).
+
+Theorem plus_equivalent : plus_recursive = plus_rec.
+  reflexivity.
+Qed.
 
 (** Going even further down the rabbit hole, [nat_rect] itself is not even a primitive.  It is a functional program that we can write manually. *)