diff --git a/.github/workflows/ci-tools.yml b/.github/workflows/ci-tools.yml
index 58bae50e0..fcbb95f0d 100644
--- a/.github/workflows/ci-tools.yml
+++ b/.github/workflows/ci-tools.yml
@@ -60,4 +60,4 @@ jobs:
           lake -R exe cache get
           lake build AliveExamples
           (cd SSA/Projects/InstCombine/; ./update_alive_statements.py)
-          # Disabled due to https://github.com/opencompl/lean-mlir/issues/660 - bash -c '! git diff | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash
+          bash -c '! git diff | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash
diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
index b2472611a..6ee67f5a7 100644
--- a/SSA/Projects/InstCombine/AliveStatements.lean
+++ b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -102,8 +102,6 @@ theorem bv_AddSub_1556 :
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
-  stop
-  /-issue 660: https://github.com/opencompl/lean-mlir/issues/660-/
   try alive_auto
   all_goals sorry
 
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 6428cef14..09c426a40 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -160,6 +160,12 @@ theorem width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
     subst h
     simp
 
+@[simp]
+lemma sub_eq_xor (a b : BitVec 1) : a - b = a ^^^ b := by
+  have ha : a = 0 ∨ a = 1 := width_one_cases _
+  have hb : b = 0 ∨ b = 1 := width_one_cases _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 @[simp]
 lemma add_eq_xor (a b : BitVec 1) : a + b = a ^^^ b := by
   have ha : a = 0 ∨ a = 1 := width_one_cases _