--- a/src/Axioms.v	Sun Nov 09 14:24:31 2008 -0500
+++ b/src/Axioms.v	Sun Nov 09 15:15:41 2008 -0500
@@ -9,9 +9,28 @@
 
 (* Additional axioms not in the Coq standard library *)
 
+Set Implicit Arguments.
+
 Axiom ext_eq : forall (A : Type) (B : A -> Type)
   (f g : forall x, B x),
   (forall x, f x = g x)
   -> f = g.
 
-Ltac ext_eq := apply ext_eq; intro.
+Theorem ext_eq_Set : forall (A : Set) (B : A -> Set)
+  (f g : forall x, B x),
+  (forall x, f x = g x)
+  -> f = g.
+  intros.
+  rewrite (ext_eq _ _ _ H); reflexivity.
+Qed.
+
+Theorem ext_eq_forall : forall (A : Type)
+  (f g : A -> Set),
+  (forall x, f x = g x)
+  -> @eq Type (forall x, f x) (forall x, g x).
+  intros.
+  rewrite (ext_eq _ _ _ H); trivial.
+Qed.
+
+Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
+  || apply ext_eq_forall); intro.