--- a/Makefile	Mon Nov 30 15:41:51 2009 -0500
+++ b/Makefile	Fri Dec 04 13:44:05 2009 -0500
@@ -2,7 +2,7 @@
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Generic Universes Match Reflection \
-	Firstorder Hoas Interps Extensional Intensional Impure
+	Large Firstorder Hoas Interps Extensional Intensional Impure
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)

--- a/src/Intro.v	Mon Nov 30 15:41:51 2009 -0500
+++ b/src/Intro.v	Fri Dec 04 13:44:05 2009 -0500
@@ -207,6 +207,8 @@
 \hline
 Proof by Reflection & \texttt{Reflection.v} \\
 \hline
+Proving in the Large & \texttt{Large.v} \\
+\hline
 First-Order Abstract Syntax & \texttt{Firstorder.v} \\
 \hline
 Higher-Order Abstract Syntax & \texttt{Hoas.v} \\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Large.v	Fri Dec 04 13:44:05 2009 -0500
@@ -0,0 +1,74 @@
+(* Copyright (c) 2009, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import Tactics.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{Proving in the Large}% *)
+
+
+(** * Modules *)
+
+Module Type GROUP.
+  Parameter G : Set.
+  Parameter f : G -> G -> G.
+  Parameter e : G.
+  Parameter i : G -> G.
+
+  Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
+  Axiom ident : forall a, f e a = a.
+  Axiom inverse : forall a, f (i a) a = e.
+End GROUP.
+
+Module Type GROUP_THEOREMS.
+  Declare Module M : GROUP.
+
+  Axiom ident' : forall a, M.f a M.e = a.
+
+  Axiom inverse' : forall a, M.f a (M.i a) = M.e.
+
+  Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
+End GROUP_THEOREMS.
+
+Module Group (M : GROUP) : GROUP_THEOREMS.
+  Module M := M.
+
+  Import M.
+
+  Theorem inverse' : forall a, f a (i a) = e.
+    intro.
+    rewrite <- (ident (f a (i a))).
+    rewrite <- (inverse (f a (i a))) at 1.
+    rewrite assoc.
+    rewrite assoc.
+    rewrite <- (assoc (i a) a (i a)).
+    rewrite inverse.
+    rewrite ident.
+    apply inverse.
+  Qed.
+
+  Theorem ident' : forall a, f a e = a.
+    intro.
+    rewrite <- (inverse a).
+    rewrite <- assoc.
+    rewrite inverse'.
+    apply ident.
+  Qed.
+
+  Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
+    intros.
+    rewrite <- (H e).
+    symmetry.
+    apply ident'.
+  Qed.
+End Group.

--- a/src/toc.html	Mon Nov 30 15:41:51 2009 -0500
+++ b/src/toc.html	Fri Dec 04 13:44:05 2009 -0500
@@ -17,6 +17,7 @@
 <li><a href="Universes.html">Universes and Axioms</a>
 <li><a href="Match.html">Proof Search in Ltac</a>
 <li><a href="Reflection.html">Proof by Reflection</a>
+<li><a href="Large.html">Proving in the Large</a>
 <li><a href="Firstorder.html">First-Order Abstract Syntax</a>
 <li><a href="Hoas.html">Higher-Order Abstract Syntax</a>
 <li><a href="Interps.html">Type-Theoretic Interpreters</a>