diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index b4ae3c519e..29a4872a65 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -63,6 +63,9 @@ else oldS.map.fold
       | some fvarId'' => m.insert fvarId fvarId'')
   newS
 
+def domain (s : FVarSubst) : List FVarId :=
+s.map.fold (fun r k v => k :: r) []
+
 end FVarSubst
 end Meta