--- a/src/Coinductive.v	Thu Jul 26 19:05:12 2012 -0400
+++ b/src/Coinductive.v	Fri Jul 27 15:41:06 2012 -0400
@@ -543,10 +543,9 @@
 
 Definition var := nat.
 
-(** We define a type [vars] of maps from variables to values.  To define a function [set] for setting a variable's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
+(** We define a type [vars] of maps from variables to values.  To define a function [set] for setting a variable's value in a map, we use the standard library function [beq_nat] for comparing natural numbers. *)
 
 Definition vars := var -> nat.
-Require Import Arith.
 Definition set (vs : vars) (v : var) (n : nat) : vars :=
   fun v' => if beq_nat v v' then n else vs v'.