diff --git a/_CoqProject b/_CoqProject
index 2a786e26a0b485d5b2dfedd24e53146cf4d138e2..8fcb2177f5fa64098e0247e6eeae67ed1f4c4995 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -43,6 +43,7 @@ theories/lib/counter.v
 theories/lib/Y.v
 theories/lib/assert.v
 theories/lib/list.v
+theories/lib/polyeq.v
 
 theories/examples/bit.v
 theories/examples/or.v
diff --git a/theories/lib/polyeq.v b/theories/lib/polyeq.v
new file mode 100644
index 0000000000000000000000000000000000000000..90ac13408e33042aa7ce4c15e8233557a6c787db
--- /dev/null
+++ b/theories/lib/polyeq.v
@@ -0,0 +1,54 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Polymorphic equality check macro. *)
+From reloc Require Import reloc typing.fundamental.
+
+Fixpoint polyeq (Ï„ : type) : val :=
+  match Ï„ with
+  | TUnit => λ: "x" "y", #true
+  | TNat => λ: "x" "y", "x" = "y"
+  | TBool => λ: "x" "y", "x" = "y"
+  | TSum τ1 τ2 => λ: "x" "y",
+                  match: "x" with
+                    InjL "x" =>
+                    match: "y" with
+                      InjL "y" => (polyeq Ï„1) "x" "y"
+                    | InjR <> => #false
+                    end
+                  | InjR "x" =>
+                    match: "y" with
+                      InjL <> => #false
+                    | InjR "y" => (polyeq Ï„2) "x" "y"
+                    end
+                  end
+  | TProd τ1 τ2 => λ: "x" "y", polyeq τ1 (Fst "x") (Fst "y") &&
+                               polyeq Ï„2 (Snd "x") (Snd "y")
+  | TRef _ => λ: "x" "y", "x" = "y"
+  | _ => λ: "x" "y", #false
+  end.
+
+Section proof.
+  Context `{!relocG Σ}.
+
+  Lemma polyeq_true Ï„ v1 v2 :
+    EqType τ →
+    interp τ [] v1 v2 -∗
+    REL polyeq Ï„ v1 v2 << #true : lrel_bool.
+  Proof.
+    intros HÏ„ ; revert v1 v2. induction HÏ„=> v1 v2 /=.
+    - iDestruct 1 as "[-> ->]". rel_pures_l. rel_values.
+    - iDestruct 1 as (z) "[-> ->]". rel_pures_l.
+      rewrite bool_decide_true//. rel_values.
+    - iDestruct 1 as (z) "[-> ->]". rel_pures_l.
+      rewrite bool_decide_true//. rel_values.
+    - iDestruct 1 as (w1 w2 u1 u2 -> ->) "[Hw Hu]". rel_pures_l.
+      rewrite IHHÏ„1 IHHÏ„2.
+      rel_bind_r _.
+      rel_bind_l (polyeq Ï„ _ _). iApply (refines_bind with "Hw").
+      iIntros (v v'). iDestruct 1 as (b) "[-> ->]". simpl.
+      destruct b; rel_pures_l; eauto. rel_values.
+    - iDestruct 1 as (w1 w2) "[(->&->&H)|(->&->&H)]"; rel_pures_l.
+      + by iApply IHHÏ„1.
+      + by iApply IHHÏ„2.
+  Qed.
+
+End proof.