diff --git a/src/api/lean_univ.h b/src/api/lean_univ.h
index 865c5a01af..e6d00d83e6 100644
--- a/src/api/lean_univ.h
+++ b/src/api/lean_univ.h
@@ -90,12 +90,30 @@ lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex);
 /** \brief Store in \c r the normal for of the given universe */
 lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex);
 
-/** \brief Instantiate the universe parameters names <tt>ns[i]</tt> with <tt>us[i]</tt> in \c u,
+LEAN_DEFINE_TYPE(lean_list_univ);
+
+/** \brief Create the empty list of univs */
+lean_bool lean_list_univ_mk_nil(lean_list_univ * r, lean_exception * ex);
+/** \brief Create the list <tt>h :: t</tt> */
+lean_bool lean_list_univ_mk_cons(lean_univ h, lean_list_univ t, lean_list_univ * r, lean_exception * ex);
+/** \brief Delete/dispose the given list of univs */
+void lean_list_univ_del(lean_list_univ l);
+/** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
+lean_bool lean_list_univ_is_cons(lean_list_univ l);
+/** \brief Return true iff the two given lists are equal */
+lean_bool lean_list_univ_eq(lean_list_univ n1, lean_list_univ n2);
+/** \brief Store in \c r the head of the given list
+    \pre lean_list_univ_is_cons(l) */
+lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex);
+/** \brief Store in \c r the tail of the given list
+    \pre lean_list_univ_is_cons(l) */
+lean_bool lean_list_univ_tail(lean_list_univ l, lean_list_univ * r, lean_exception * ex);
+
+/** \brief Instantiate the universe parameters names in <tt>ns</tt> with <tt>us</tt> in \c u,
     and store the result in \c r.
-    \remark \c ns and \c us are arrays of names and universes, and both have size \c sz.
+    \remark The given lists must have the same length.
 */
-lean_bool lean_univ_instantiate(lean_univ u, unsigned sz, lean_name const * ns, lean_univ const * us,
-                                lean_univ * r, lean_exception * ex);
+lean_bool lean_univ_instantiate(lean_univ u, lean_list_name ns, lean_list_univ us, lean_univ * r, lean_exception * ex);
 
 /*@}*/
 /*@}*/
diff --git a/src/api/univ.cpp b/src/api/univ.cpp
index 2743c42981..02f8a11763 100644
--- a/src/api/univ.cpp
+++ b/src/api/univ.cpp
@@ -179,18 +179,61 @@ lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex) {
     LEAN_CATCH;
 }
 
+lean_bool lean_list_univ_mk_nil(lean_list_univ * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_list_level(new list<level>());
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_univ_mk_cons(lean_univ h, lean_list_univ t, lean_list_univ * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(h);
+    check_nonnull(t);
+    *r = of_list_level(new list<level>(to_level_ref(h), to_list_level_ref(t)));
+    LEAN_CATCH;
+}
+
+void lean_list_univ_del(lean_list_univ l) {
+    delete to_list_level(l);
+}
+
+lean_bool lean_list_univ_is_cons(lean_list_univ l) {
+    return l && !is_nil(to_list_level_ref(l));
+}
+
+lean_bool lean_list_univ_eq(lean_list_univ l1, lean_list_univ l2) {
+    return l1 && l2 && to_list_level_ref(l1) == to_list_level_ref(l2);
+}
+
+lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    if (!lean_list_univ_is_cons(l))
+        throw lean::exception("invalid argument, non-nil list expected");
+    *r = of_level(new level(head(to_list_level_ref(l))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_univ_tail(lean_list_univ l, lean_list_univ * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    if (!lean_list_univ_is_cons(l))
+        throw lean::exception("invalid argument, non-nil list expected");
+    *r = of_list_level(new list<level>(tail(to_list_level_ref(l))));
+    LEAN_CATCH;
+}
+
 /** \brief Instantiate the universe parameters names <tt>ns[i]</tt> with <tt>us[i]</tt> in \c u,
     and store the result in \c r.
     \remark \c ns and \c us are arrays of names and universes, and both have size \c sz.
 */
-lean_bool lean_univ_instantiate(lean_univ u, unsigned sz, lean_name const * ns, lean_univ const * us,
-                                lean_univ * r, lean_exception * ex) {
+lean_bool lean_univ_instantiate(lean_univ u, lean_list_name ns, lean_list_univ us, lean_univ * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(u);
-    buffer<name> tmp_ns;
-    buffer<level> tmp_us;
-    to_buffer(sz, ns, tmp_ns);
-    to_buffer(sz, us, tmp_us);
-    *r = of_level(new level(instantiate(to_level_ref(u), to_list(tmp_ns), to_list(tmp_us))));
+    check_nonnull(ns);
+    check_nonnull(us);
+    if (length(to_list_name_ref(ns)) != length(to_list_level_ref(us)))
+        throw lean::exception("invalid arguments, the given lists must have the same length");
+    *r = of_level(new level(instantiate(to_level_ref(u), to_list_name_ref(ns), to_list_level_ref(us))));
     LEAN_CATCH;
 }
diff --git a/src/api/univ.h b/src/api/univ.h
index 4129d1c4bd..0f093a0514 100644
--- a/src/api/univ.h
+++ b/src/api/univ.h
@@ -15,4 +15,8 @@ inline level * to_level(lean_univ n) { return reinterpret_cast<level *>(n); }
 inline level const & to_level_ref(lean_univ n) { return *reinterpret_cast<level *>(n); }
 inline lean_univ of_level(level * n) { return reinterpret_cast<lean_univ>(n); }
 void to_buffer(unsigned sz, lean_univ const * us, buffer<level> & r);
+
+inline list<level> * to_list_level(lean_list_univ n) { return reinterpret_cast<list<level> *>(n); }
+inline list<level> const & to_list_level_ref(lean_list_univ n) { return *reinterpret_cast<list<level> *>(n); }
+inline lean_list_univ of_list_level(list<level> * n) { return reinterpret_cast<lean_list_univ>(n); }
 }
diff --git a/src/tests/shared/univ.c b/src/tests/shared/univ.c
index 8a55c6d622..23bb4a307d 100644
--- a/src/tests/shared/univ.c
+++ b/src/tests/shared/univ.c
@@ -22,6 +22,8 @@ int main() {
     lean_name a, l, U, pp, pp_unicode, rn;
     lean_options o1, o2;
     lean_univ zero, one, p1, g1, m1, u, n, i, ru;
+    lean_list_name ln1, ln2;
+    lean_list_univ lu1, lu2;
     char const * s1;
     lean_bool r;
 
@@ -48,7 +50,15 @@ int main() {
     check(lean_univ_geq(one, zero, &r, &ex) && r);
 
     /* replace l_1 with one in u */
-    check(lean_univ_instantiate(u, 1, &l, &one, &i, &ex));
+    check(lean_list_name_mk_nil(&ln1, &ex));
+    check(lean_list_name_mk_cons(l, ln1, &ln2, &ex));
+    check(lean_list_univ_mk_nil(&lu1, &ex));
+    check(lean_list_univ_mk_cons(one, lu1, &lu2, &ex));
+    check(lean_univ_instantiate(u, ln2, lu2, &i, &ex));
+    lean_list_name_del(ln1);
+    lean_list_name_del(ln2);
+    lean_list_univ_del(lu1);
+    lean_list_univ_del(lu2);
     lean_string_del(s1);
     check(lean_univ_to_string_using(i, o2, &s1, &ex));
     printf("universe: %s\n", s1);