diff --git a/_CoqProject b/_CoqProject
index f501a6ea40b30d526552cfc3859e9cb4c99e5b45..033fbd5de6c5b0189b71cab7a402acb849240858 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -23,3 +23,4 @@ theories/logrel/session_types.v
 theories/logrel/types.v
 theories/logrel/subtyping.v
 theories/logrel/examples/double.v
+theories/logrel/examples/pair.v
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
new file mode 100644
index 0000000000000000000000000000000000000000..aea603bb2bf8ec27046faf572840699429d5cd0e
--- /dev/null
+++ b/theories/logrel/examples/pair.v
@@ -0,0 +1,18 @@
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import channel proto proofmode.
+From actris.logrel Require Export types.
+
+Definition prog : expr := λ: "c", (recv "c", recv "c").
+
+Section pair.
+  Context `{heapG Σ, chanG Σ}.
+
+  Lemma prog_typed :
+    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
+  Proof.
+    rewrite /prog.
+    iApply ltyped_lam. iApply ltyped_pair.
+    iApply ltyped_recv. iApply ltyped_recv.
+  Qed.
+
+End pair.