--- a/src/Equality.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Equality.v	Fri Nov 06 12:15:05 2009 -0500
@@ -177,6 +177,8 @@
 
     destruct a0.
 
+    ]]
+
     [[
 User error: Cannot solve a second-order unification problem
 ]]
@@ -187,6 +189,8 @@
 
     assert (a0 = refl_equal _).
 
+    ]]
+
     [[
 The term "refl_equal ?98" has type "?98 = ?98"
  while it is expected to have type "a = elm"
@@ -256,6 +260,8 @@
     (** [[
 
     simple destruct pf.
+
+    ]]
     
       [[
 
@@ -282,6 +288,8 @@
     (** [[
 
     simple destruct pf.
+
+    ]]
     
       [[
 
@@ -299,6 +307,8 @@
         | refl_equal => refl_equal _
       end.
 
+      ]]
+
      [[
 
 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
@@ -380,6 +390,8 @@
     (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
     fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
 
+    ]]
+
      [[
 
 The term
@@ -415,6 +427,8 @@
        [[
     case pf.
 
+    ]]
+
        [[
 
 User error: Cannot solve a second-order unification problem
@@ -454,6 +468,8 @@
 
     rewrite (UIP_refl _ _ pf).
 
+    ]]
+
        [[
 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
  while it is expected to have type "?556 = ?556"
@@ -645,6 +661,8 @@
 
     rewrite IHls1.
 
+    ]]
+
        [[
 
 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
@@ -764,6 +782,8 @@
 
    Theorem S_eta : S = (fun n => S n).
 
+   ]]
+
    Unfortunately, this theorem is not provable in CIC without additional axioms.  None of the definitional equality rules force function equality to be %\textit{%#<i>#extensional#</i>#%}%.  That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal.  We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
 
 (* begin thide *)