diff --git a/theories/opt/foo.v b/theories/opt/foo.v
index 3d06192c7ad76a04d0374ce0ee94a36228f1f2c4..f37914b51c8fbeea22b386c1ecd78f08ecce0ede 100644
--- a/theories/opt/foo.v
+++ b/theories/opt/foo.v
@@ -1,4 +1,4 @@
-From stbor.lang Require Import defs.
+From stbor.lang Require Import defs steps_inversion.
 From stbor.sim Require Import local invariant.
 
 Definition sim_body := sim_local_body wsat vrel_expr.