diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index caaacf7244..0e64bfe0d5 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -59,11 +59,11 @@ extern "C" object * lean_expr_instantiate(object * a0, object * subst) {
                 nat const & vidx = bvar_idx(m);
                 if (vidx >= offset) {
                     size_t h = offset + n;
-                    if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) {
+                    if (h < offset /* overflow, h is bigger than any vidx */ || (vidx.is_small() && vidx.get_small_value() < h)) {
                         expr v(lean_array_get_core(subst, vidx.get_small_value() - offset), true);
                         return some_expr(lift_loose_bvars(v, offset));
                     } else {
-                        return some_expr(mk_bvar(vidx - nat(n)));
+                        return some_expr(mk_bvar(vidx - nat::of_size_t(n)));
                     }
                 }
             }
@@ -82,7 +82,7 @@ expr instantiate_rev(expr const & a, unsigned n, expr const * subst) {
                 nat const & vidx = bvar_idx(m);
                 if (vidx >= offset) {
                     size_t h = offset + n;
-                    if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) {
+                    if (h < offset /* overflow, h is bigger than any vidx */ || (vidx.is_small() && vidx.get_small_value() < h)) {
                         return some_expr(lift_loose_bvars(subst[n - (vidx.get_small_value() - offset) - 1], offset));
                     } else {
                         return some_expr(mk_bvar(vidx - nat(n)));
@@ -107,11 +107,11 @@ extern "C" object * lean_expr_instantiate_rev(object * a0, object * subst) {
                 nat const & vidx = bvar_idx(m);
                 if (vidx >= offset) {
                     size_t h = offset + n;
-                    if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) {
+                    if (h < offset /* overflow, h is bigger than any vidx */ || (vidx.is_small() && vidx.get_small_value() < h)) {
                         expr v(lean_array_get_core(subst, n - (vidx.get_small_value() - offset) - 1), true);
                         return some_expr(lift_loose_bvars(v, offset));
                     } else {
-                        return some_expr(mk_bvar(vidx - nat(n)));
+                        return some_expr(mk_bvar(vidx - nat::of_size_t(n)));
                     }
                 }
             }
diff --git a/src/util/nat.h b/src/util/nat.h
index d71d4f3bfb..28ca4f5a09 100644
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -25,6 +25,8 @@ public:
         if (m > 0)
             *this = nat(mk_nat_obj(m));
     }
+    static nat of_size_t(size_t v) { return nat(lean_usize_to_nat(v)); }
+
     nat(nat const & other):object_ref(other) {}
     nat(nat && other):object_ref(other) {}