diff --git a/Bytecode/Basic.lean b/Bytecode/Basic.lean
index 2b6aa4f..4b39b5c 100644
--- a/Bytecode/Basic.lean
+++ b/Bytecode/Basic.lean
@@ -62,9 +62,9 @@ def M.run (m : M Unit) : Option Rat :=
 theorem M.push_pop : (do push x; pop) = pure x := by
   funext xs
   -- what on earth
-  simp only [bind, OptionT.bind, OptionT.mk, StateT.bind, push, modify, modifyGet,
+  simp [bind, OptionT.bind, OptionT.mk, StateT.bind, push, modify, modifyGet,
     MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, OptionT.lift, StateT.modifyGet, pure,
-    StateT.pure, pop, getModify, Array.pop_push, Array.back?_push, OptionT.pure]
+    StateT.pure, pop, getModify, OptionT.pure]
 
 theorem Ast.compile_eq_push_interpret (ast : Ast)
     : ast.compile = M.push ast.interpret := by