diff --git a/theories/Data/Map/FMapTwoThreeK.v b/theories/Data/Map/FMapTwoThreeK.v
index 0335454..e6aea59 100644
--- a/theories/Data/Map/FMapTwoThreeK.v
+++ b/theories/Data/Map/FMapTwoThreeK.v
@@ -9,7 +9,6 @@ Set Strict Implicit.
 
 Section keyed.
   Variable K : Type.
-  Variable K_le : K -> K -> Prop.
   Variable RD_K : K -> K -> comparison.
 
   Inductive twothree (T : Type) : Type :=