diff --git a/examples/peano.pg b/examples/peano.pg
index f0b3714..bca84ee 100644
--- a/examples/peano.pg
+++ b/examples/peano.pg
@@ -137,11 +137,12 @@ nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc
  * long and complicated really quickly.
  *]
 
-one : nat := suc zero;
-two : nat := suc one;
+-- Some abbreviations for common numbers.
+one   : nat := suc zero;
+two   : nat := suc one;
 three : nat := suc two;
-four : nat := suc three;
-five : nat := suc four;
+four  : nat := suc three;
+five  : nat := suc four;
 
 -- First, the predecessor of `n` is `m` if `n = suc m`.
 pred (n m : nat) : * := eq nat n (suc m);
@@ -150,7 +151,7 @@ pred (n m : nat) : * := eq nat n (suc m);
 szc_l (n : nat) := eq nat n zero;
 
 -- The second option is that `n` has a predecessor.
-szc_r (n : nat) := exists nat (fun (m : nat) => pred n m);
+szc_r (n : nat) := exists nat (pred n);
 
 -- So the claim we are trying to prove is that either one of the above options
 -- holds for every `n`.
@@ -192,41 +193,50 @@ suc_or_zero : forall (n : nat), szc n :=
 -- For any such equations, there exists a function.
 rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
 
+-- Here's equation one.
 rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) := 
   eq A (f zero) fzero;
 
+-- And equation two.
 rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
   forall (n : nat) (y : A),
     eq A (f n) y -> eq A (f (suc n)) (fsuc n y);
 
 -- Said function satisfies the equations.
--- Equation 1.
+-- It satisfies equation one.
 rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) :
   rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom;
 
--- Equation 2.
+-- And two.
 rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) :
   rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom;
 
 -- And, finally, this function is unique in the sense that if any other function
--- satisfies the equations, it is really `rec_def`.
+-- also satisfies the equations, it takes the same values as `rec_def`.
 rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
   rec_cond_zero A fzero fsuc f ->
-  rec_cond_suc A fzero fsuc f ->
+  rec_cond_suc  A fzero fsuc f ->
   rec_cond_zero A fzero fsuc g ->
-  rec_cond_suc A fzero fsuc g ->
+  rec_cond_suc  A fzero fsuc g ->
   forall (x : nat), eq A (f x) (g x) := axiom;
 
 -- Now we can safely define addition.
+
+-- First, here's the RHS of equation 2 as a function, since it will show up
+-- multiple times.
 psuc (_ r : nat) := suc r;
 
+-- And here's `plus`!
 plus (n : nat) : nat -> nat := rec_def nat n psuc;
 
--- n + 0 = n
+-- The first equation manifests itself as the familiar
+--      n + 0 = 0.
 plus_0_r (n : nat) : eq nat (plus n zero) n :=
   rec_def_sat_zero nat n psuc;
 
--- n + suc m = suc (n + m)
+-- The second equation, after a bit of massaging, manifests itself as the
+-- likewise familiar
+--      n + suc m = suc (n + m).
 plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
   rec_def_sat_suc nat n psuc m (plus n m) (eq_refl nat (plus n m));