diff --git a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
index 91b979d7..ecc407fd 100644
--- a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
@@ -132,7 +132,6 @@ Module Aggregate.
       Proof using MOD.
         verify_spec. wapply op_eq_ok.
         go using prim.primR_aggressiveC.
-        by [].
       Qed.
       Definition op_neq_B := [LINK] op_neq_ok.