diff --git a/SSA/Core/HVector.lean b/SSA/Core/HVector.lean
index 78f122e46..30ff778f0 100644
--- a/SSA/Core/HVector.lean
+++ b/SSA/Core/HVector.lean
@@ -115,6 +115,9 @@ theorem eq_of_type_eq_nil {A : α → Type*} {l : List α}
   cases h; cases t₁; cases t₂; rfl
 syntax "[" withoutPosition(term,*) "]ₕ"  : term
 
+@[simp]
+theorem cons_nil_get : (HVector.cons x .nil).get (0 : Fin 1) = x := rfl
+
 -- Copied from core for List
 macro_rules
   | `([ $elems,* ]ₕ) => do
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
index f3cde072c..444b8e5e4 100644
--- a/SSA/Projects/InstCombine/Tactic.lean
+++ b/SSA/Projects/InstCombine/Tactic.lean
@@ -70,7 +70,7 @@ macro "simp_alive_ssa" : tactic =>
 
         simp (config := {failIfUnchanged := false}) only [
             InstCombine.Op.denote, HVector.getN, HVector.get,
-            beq_self_eq_true, Option.isSome_some
+            beq_self_eq_true, Option.isSome_some, HVector.cons_nil_get
           ]
 
         -- Fold integers into their canonical form.