diff --git a/SSA/Projects/LLVMRiscV/PeepholeRefine.lean b/SSA/Projects/LLVMRiscV/PeepholeRefine.lean
index 82233cac80..93b56aec5c 100644
--- a/SSA/Projects/LLVMRiscV/PeepholeRefine.lean
+++ b/SSA/Projects/LLVMRiscV/PeepholeRefine.lean
@@ -31,6 +31,8 @@ structure LLVMPeepholeRewriteRefine (w : Nat) (Γ : List Ty) where
     PoisonOr.IsRefinedBy (lhs.denote V |>.getN 0) (rhs.denote V |>.getN 0) := by
       simp_lowering <;> bv_decide
 
+axiom refinement_correctness {p: Prop} : p
+
 /-- `LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND` is a wrapper to pass the rewrites to the
   Peephole Rewriter, with a `sorry` replacing the correctness proof which cannot be provided,
   given that we are working with refinement semantics. -/
@@ -40,7 +42,7 @@ def LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND
   {
     lhs := self.lhs
     rhs := self.rhs
-    correct := by sorry
+    correct := refinement_correctness
   }
 
 @[simp_riscv] lemma toType_bv : TyDenote.toType (Ty.riscv (.bv)) = BitVec 64 := rfl