diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index e5f2d43..b1133fe 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -53,15 +53,6 @@
   	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc.hpp))
 )
-(subdir mutex
- (rule
-  (targets test_cpp.v.stderr test_cpp.v)
-  (alias test_ast)
-  (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe))
-  (action
-  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
- (alias (name srcs) (deps test.cpp))
-)
 (subdir new
  (rule
   (targets inc_new_cpp.v.stderr inc_new_cpp.v)
diff --git a/rocq-brick-libstdcpp/proof/mutex/inc.hpp b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
index 5f56386..ff041bd 100644
--- a/rocq-brick-libstdcpp/proof/mutex/inc.hpp
+++ b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
@@ -2,8 +2,3 @@
 
 template class std::lock_guard<std::mutex>;
 template class std::scoped_lock<std::mutex, std::mutex>;
-
-inline void foo() {
-  std::mutex m1, m2;
-  std::scoped_lock lock(m1, m2);
-}
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v
index 86814ab..d07e1ae 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec.v
@@ -1,3 +1,4 @@
 Require Export skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Export skylabs.brick.libstdcpp.mutex.spec.lock_guard.
 Require Export skylabs.brick.libstdcpp.mutex.spec.recursive_mutex.
+Require Export skylabs.brick.libstdcpp.mutex.spec.scoped_lock.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v b/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
index e80a4bf..a395a1b 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
@@ -33,10 +33,15 @@ Module lock_guard.
   Fail #[only(cfractional,cfracvalid,ascfractional)] derive R.
 
   #[only(cfracvalid)] derive R.
+
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context {HAS_THREADS : HasStdThreads Σ}.
 
+  #[global] Instance R_learn :
+    Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) lock_guard.R) :=
+    ltac:(solve_learnable).
+
   Set Printing Coercions.
 
   Section with_R_cfrac'.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
index 5f42cc3..cd2c506 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
@@ -57,19 +57,6 @@ Module scoped_lock.
           mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
           mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
       ).
-
-      cpp.spec "foo()" as foo_spec from source with
-      (
-        \persist{thr} current_thread thr
-        \post emp
-      ).
-
-      Lemma foo_ok : verify[source] foo_spec.
-      Proof.
-        verify_spec; go.
-        iExists emp; go.
-        iExists emp; go.
-      Qed.
     End with_threads.
   End with_cpp.
 
diff --git a/rocq-brick-libstdcpp/proof/mutex/test.cpp b/rocq-brick-libstdcpp/proof/mutex/test.cpp
deleted file mode 100644
index 6c32bb5..0000000
--- a/rocq-brick-libstdcpp/proof/mutex/test.cpp
+++ /dev/null
@@ -1,16 +0,0 @@
-#include "inc.hpp"
-
-using namespace std;
-
-void test() {
-  std::mutex m;
-  m.lock();
-  m.unlock();
-}
-
-void test2() {
-  std::mutex m;
-  {
-    std::lock_guard<std::mutex> lm(m);
-  }
-}
diff --git a/rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v
deleted file mode 100644
index 1e956c8..0000000
--- a/rocq-brick-libstdcpp/proof/mutex/test_cpp_proof.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Require Import skylabs.auto.cpp.prelude.proof.
-Require Import skylabs.brick.libstdcpp.mutex.test_cpp.
-Require Import skylabs.brick.libstdcpp.mutex.spec.
-
-Section with_cpp.
-  Context `{Σ : cpp_logic} {HAS_THREADS : HasStdThreads Σ}.
-  Context `{MOD : test_cpp.source ⊧ σ}. (* σ is the whole program *)
-
-  cpp.spec "test()" as test_spec with
-      (\post emp).
-
-  Theorem test_ok : verify[source] test_spec.
-  Proof using HAS_THREADS.
-    verify_spec; go.
-    iExists emp; go.
-  Qed.
-
-End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
index 7e1c50a..916b195 100644
--- a/rocq-brick-libstdcpp/test/dune.inc
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -80,6 +80,15 @@
   	 (with-stderr-to N6_print_sizeof_cpp.v.stderr (run cpp2v -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps N6_print_sizeof.cpp))
 )
+(subdir mutex
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v)
+  (alias test_ast)
+  (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir new
  (rule
   (targets demo_cpp.v.stderr demo_cpp.v)
diff --git a/rocq-brick-libstdcpp/test/mutex/test.cpp b/rocq-brick-libstdcpp/test/mutex/test.cpp
new file mode 100644
index 0000000..1ad08c5
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/mutex/test.cpp
@@ -0,0 +1,21 @@
+#include <mutex>
+
+using namespace std;
+
+void test_mutex() {
+  std::mutex m;
+  m.lock();
+  m.unlock();
+}
+
+void test_lock_guard() {
+  std::mutex m;
+  {
+    std::lock_guard<std::mutex> lm(m);
+  }
+}
+
+void test_scoped_lock() {
+  std::mutex m1, m2;
+  std::scoped_lock lock(m1, m2);
+}
diff --git a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
new file mode 100644
index 0000000..ffe7ef4
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
@@ -0,0 +1,32 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.spec.
+Require Import skylabs.brick.libstdcpp.test.mutex.test_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv} {HAS_THREADS : HasStdThreads Σ}.
+
+  cpp.spec "test_mutex()" as test_mutex_spec from source with (\post emp).
+
+  Theorem test_mutex_ok : verify[source] "test_mutex()".
+  Proof.
+    verify_spec; go.
+    iExists emp; go.
+  Qed.
+
+  cpp.spec "test_lock_guard()" as test_lock_guard_spec from source with (\post emp).
+
+  Lemma test_lock_guard_ok : verify[source] "test_lock_guard()".
+  Proof.
+    verify_spec; go.
+    iExists emp; go.
+  Qed.
+
+  cpp.spec "test_scoped_lock()" as test_scoped_lock_spec from source with (\post emp).
+
+  Lemma test_scoped_lock_ok : verify[source] "test_scoped_lock()".
+  Proof.
+    verify_spec; go.
+    iExists emp; go.
+    iExists emp; go.
+  Qed.
+End with_cpp.