diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index e0fb845e2..84dce8854 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -950,6 +950,9 @@ external pred coq.univ.print .
 % [coq.univ.new U] A fresh universe.
 external pred coq.univ.new o:univ.
 
+% [coq.univ.super U U1] relates a univ U to its successor U1
+external pred coq.univ.super i:univ, o:univ.
+
 % [coq.univ Name U] Finds a named unvierse. Can fail.
 external pred coq.univ o:id, o:univ.
 
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 644b5f8ff..3a710a7ec 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -2236,6 +2236,14 @@ phase unnecessary.|};
      state, !: u, [])),
   DocAbove);
 
+  MLCode(Pred("coq.univ.super",
+    In(univ,"U",
+    Out(univ,"U1",
+    Full(unit_ctx,  "relates a univ U to its successor U1"))),
+  (fun u _ ~depth _ _ state ->
+    state, !: (Univ.Universe.super u), [])),
+  DocAbove);
+
   MLCode(Pred("coq.univ",
     InOut(B.ioarg id, "Name",
     InOut(B.ioarg univ, "U",