diff --git a/encodings/pairs.lp b/encodings/pairs.lp
new file mode 100644
index 0000000000000000000000000000000000000000..caba304b4df368ccae523cdbda6922757b9171af
--- /dev/null
+++ b/encodings/pairs.lp
@@ -0,0 +1,16 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
+require open personoj.encodings.tuple
+require open personoj.encodings.prenex
+
+set declared "Σ"
+
+constant symbol Σ (t: Set): (η t → Set) → Set
+symbol pair_ss {t: Set} {u: η t → Set} (m: η t): η (u m) → η (Σ t u)
+
+symbol fst_ss {t: Set} {u: η t → Set}: η (Σ t u) → η t
+symbol snd_ss {t: Set} {u: η t → Set} (m: η (Σ t u)): η (u (fst_ss m))
+
+rule fst_ss (pair_ss $m _) ↪ $m
+rule snd_ss (pair_ss _ $n) ↪ $n
diff --git a/tests/pairs.lp b/tests/pairs.lp
new file mode 100644
index 0000000000000000000000000000000000000000..869f3d4193bad1fb08bce14d57707c0c56e01cff
--- /dev/null
+++ b/tests/pairs.lp
@@ -0,0 +1,15 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.deptype
+require open personoj.encodings.prenex
+require open personoj.encodings.pairs
+
+symbol nat: Set
+symbol plus: η ((Σ nat (λ_, nat)) ~> nat)
+
+symbol z: η nat
+symbol s: η (nat ~> nat)
+set builtin "0" ≔ z
+set builtin "+1" ≔ s
+
+assert plus (pair_ss 3 4): η nat