1 files changed, 9 insertions, 0 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index c23ed601..7a301929 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1547,6 +1547,15 @@ Proof.
   intros until b.
   intro Hop; injection Hop; clear Hop; intro; subst a.
   intros HeL He1 He2 HeC.
+  destruct same_expr_pure eqn:SAME.
+  {
+    destruct (eval_same_expr a1 a2 le v1 v2 SAME He1 He2) as [EQ1 EQ2].
+    subst a2. subst v2.
+    exists v1; split; trivial.
+    cbn.
+    rewrite if_same.
+    apply Val.lessdef_normalize.
+  }
   unfold cond_to_condition0.
   destruct (cond_to_condition0_match cond al).
   {