diff --git a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
index 42971213a..a1b1ac340 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
@@ -60,12 +60,13 @@ theorem alive_DivRemOfSelect (w : Nat) :
     LLVM.const?, LLVM.icmp?,
     HVector.toTuple, List.nthLe, bitvec_minus_one]
   intro y x c
-  simp [Option.bind, bind, Monad.toBind]
+  simp only [List.length_singleton, Fin.zero_eta, List.get_cons_zero, List.map_eq_map, List.map_cons,
+    List.map_nil, CharP.cast_eq_zero, Ctxt.Valuation.snoc_last, pairBind, bind, Option.bind, Int.ofNat_eq_coe]
   clear Γv
   cases c
   -- | select condition is itself `none`, nothing more to be done. propagate the `none`.
-  . case none => cases x <;> cases y <;> simp
-  . case some cond =>
+  case none => cases x <;> cases y <;> simp
+  case some cond =>
      obtain ⟨vcond, hcond⟩ := cond
      obtain (h | h) : vcond = 1 ∨ vcond = 0 := by
        norm_num at hcond