1 files changed, 0 insertions, 6 deletions
diff --git a/lib/Maps.v b/lib/Maps.v
index 4a346c6c..4209fe6e 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1125,12 +1125,6 @@ Module EMap(X: EQUALITY_TYPE) <: MAP.
   Proof.
     intros. unfold get, map. reflexivity.
   Qed.
-  Lemma exten:
-    forall (A: Set) (m1 m2: t A),
-    (forall x: X.t, m1 x = m2 x) -> m1 = m2.
-  Proof.
-    intros. unfold t. apply extensionality. assumption.
-  Qed.
 End EMap.
 
 (** * Useful notations *)