diff --git a/_CoqProject b/_CoqProject
index bb31c07ca1de17c5678e0230cf6e0cc045220c7c..c62d7242382120df44dc189ce5881e2bf4134909 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,6 +30,7 @@ theories/tests/proofmode_tests.v
 theories/lib/lock.v
 theories/lib/counter.v
 theories/lib/Y.v
+theories/lib/assert.v
 
 theories/examples/bit.v
 theories/examples/or.v
diff --git a/theories/lib/assert.v b/theories/lib/assert.v
new file mode 100644
index 0000000000000000000000000000000000000000..a6cc2c3d2848c7d9171116a1c99ee46f54508d3a
--- /dev/null
+++ b/theories/lib/assert.v
@@ -0,0 +1,20 @@
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang.lib Require Export assert.
+From reloc Require Import proofmode.
+Set Default Proof Using "Type".
+
+Definition assert : val :=
+  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
+(* just below ;; *)
+Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
+
+(* Nested relational specifications *)
+Lemma rel_assert_l `{!relocG Σ} K e t A :
+  (∀ K t A, (REL fill K (of_val #true) << t : A) -∗ REL fill K e << t : A) -∗
+  (▷ REL fill K (of_val #()) << t : A) -∗
+  REL fill K (assert (LamV BAnon e)%V) << t : A.
+Proof.
+  iIntros "H1 H2". rel_rec_l. rel_rec_l.
+  rel_apply_l "H1". by rel_if_l.
+Qed.