diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 4db7709..3bf8c28 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -479,7 +479,7 @@ _∈k_ k m = MemProp._∈_ k (keys m)
 Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
 Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
 
-open ImplRelation renaming (subset to subset-impl)
+open ImplRelation using () renaming (subset to subset-impl) public
 
 _⊆_ : Map → Map → Set (a ⊔ℓ b)
 _⊆_ (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂