diff --git a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
index b6475a63d..468044823 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
@@ -42,6 +42,9 @@ theorem alive_DivRemOfSelect (w : Nat) :
     alive_DivRemOfSelect_src w ⊑ alive_DivRemOfSelect_tgt w := by
   unfold alive_DivRemOfSelect_src alive_DivRemOfSelect_tgt
   simp_alive_peephole
+  simp_alive_undef
+  simp_alive_ops
+  simp_alive_case_bash
   alive_auto
 
 end AliveHandwritten
diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index cecec4396..5a071ded2 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -151,8 +151,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
         have htwopow_pos : 2^w'' > 0 := Nat.pow_pos (by omega)
         rw [Nat.mod_eq_of_lt (a := 3) (by omega)]
         split
-        case h_1 c hugt => contradiction
-        case h_2 c hugt =>
+        case h_1 c hugt =>
           clear c
           have hugt :
             (1 + BitVec.toNat x) % 2 ^ Nat.succ (Nat.succ w'') < 3 := by
@@ -191,7 +190,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
                 subst heqzero
                 simp [BitVec.sdiv_zero]
           · exact intMin_neq_one (by omega)
-        case h_3 c hugt =>
+        case h_2 c hugt =>
           clear c
           simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, Nat.reducePow, Fin.zero_eta,
             Fin.isValue, ofFin_ofNat, ofNat_eq_ofNat, Option.some.injEq,
diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index f5d31610c..ec75aa21c 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -406,11 +406,11 @@ def ashr {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW
  If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
 -/
 @[simp_llvm_option]
-def select {w : Nat} (c? : IntW 1) (x? y? : IntW w ) : IntW w :=
-  match c? with
-  | none => none
-  | some true => x?
-  | some false => y?
+def select {w : Nat} (c? : IntW 1) (x? y? : IntW w ) : IntW w := do
+  let c ← c?
+  match c with
+  | 1#1 => x?
+  | 0#1 => y?
 
 inductive IntPredicate where
   | eq