diff --git a/src/coqutil/Map/Separation.v b/src/coqutil/Map/Separation.v
index 36c32f58..bfae5231 100644
--- a/src/coqutil/Map/Separation.v
+++ b/src/coqutil/Map/Separation.v
@@ -20,6 +20,12 @@ Definition sepclause_of_map {key value map} (m : @map.rep key value map)
   : map.rep -> Prop := Logic.eq m.
 Coercion sepclause_of_map : Interface.map.rep >-> Funclass.
 
+Lemma sepclause_of_map_empty {key value map} :
+  Lift1Prop.iff1 (@sepclause_of_map key value map Interface.map.empty) (emp True).
+Proof.
+  cbv [sepclause_of_map emp]; split; intuition congruence.
+Qed.
+
 Declare Scope sep_scope.
 Delimit Scope sep_scope with sep.
 Infix "*" := sep (at level 40, left associativity) : sep_scope.