diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index afe03d48b6..845c6a4f62 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -22,6 +22,7 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "library/expr_lt.h"
 #include "library/locals.h"
 #include "library/num.h"
+#include "library/idx_metavar.h"
 #include "library/util.h"
 #include "library/norm_num.h"
 #include "library/attribute_manager.h"
@@ -91,7 +92,7 @@ bool simplify_core_fn::instantiate_emetas(tmp_type_context & tmp_ctx, unsigned n
             i--;
             if (failed) return;
             expr mvar_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(mvar));
-            if (has_metavar(mvar_type)) {
+            if (has_idx_metavar(mvar_type)) {
                 failed = true;
                 return;
             }
@@ -252,7 +253,7 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const &
             expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(),
                                      local_factory.as_buffer().data());
             expr l = local_factory.push_local(binding_name(m_type), d, binding_info(m_type));
-            lean_assert(!has_metavar(l));
+            lean_assert(!has_idx_metavar(l));
             m_type = binding_body(m_type);
         }
         m_type = instantiate_rev(m_type, local_factory.as_buffer().size(), local_factory.as_buffer().data());
diff --git a/tests/lean/run/simp_univ_metavars.lean b/tests/lean/run/simp_univ_metavars.lean
new file mode 100644
index 0000000000..c6b738808c
--- /dev/null
+++ b/tests/lean/run/simp_univ_metavars.lean
@@ -0,0 +1,76 @@
+meta def blast : tactic unit := using_smt $ return ()
+
+structure { u v } Category :=
+  (Obj : Type u )
+  (Hom : Obj -> Obj -> Type v)
+  (identity : Π X : Obj, Hom X X)
+  (compose  : Π ⦃X Y Z : Obj⦄, Hom X Y → Hom Y Z → Hom X Z)
+  (left_identity  : ∀ ⦃X Y : Obj⦄ (f : Hom X Y), compose (identity _) f = f)
+
+structure Functor (C : Category) (D : Category) :=
+  (onObjects   : C^.Obj → D^.Obj)
+  (onMorphisms : Π ⦃X Y : C^.Obj⦄,
+                C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))
+
+structure NaturalTransformation { C D : Category } ( F G : Functor C D ) :=
+  (components: Π X : C^.Obj, D^.Hom (F^.onObjects X) (G^.onObjects X))
+
+definition IdentityNaturalTransformation { C D : Category } (F : Functor C D) : NaturalTransformation F F :=
+  {
+    components := λ X, D^.identity (F^.onObjects X)
+  }
+
+definition vertical_composition_of_NaturalTransformations
+  { C D : Category }
+  { F G H : Functor C D }
+  ( α : NaturalTransformation F G )
+  ( β : NaturalTransformation G H ) : NaturalTransformation F H :=
+  {
+    components := λ X, D^.compose (α^.components X) (β^.components X)
+  }
+
+-- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.
+lemma NaturalTransformations_componentwise_equal
+  { C D : Category }
+  { F G : Functor C D }
+  ( α β : NaturalTransformation F G )
+  ( w : ∀ X : C^.Obj, α^.components X = β^.components X ) : α = β :=
+  begin
+    induction α with αc,
+    induction β with βc,
+    have hc : αc = βc, from funext w,
+    by subst hc
+  end
+
+@[simp]
+lemma vertical_composition_of_NaturalTransformations_components
+  { C D : Category }
+  { F G H : Functor C D }
+  { α : NaturalTransformation F G }
+  { β : NaturalTransformation G H }
+  { X : C^.Obj } :
+  (vertical_composition_of_NaturalTransformations α β)^.components X = D^.compose (α^.components X) (β^.components X) :=
+by blast
+
+@[simp]
+lemma IdentityNaturalTransformation_components
+  { C D : Category }
+  { F : Functor C D }
+  { X : C^.Obj } :
+  (IdentityNaturalTransformation F)^.components X = D^.identity (F^.onObjects X) :=
+by blast
+
+definition FunctorCategory ( C D : Category ) : Category :=
+{
+  Obj := Functor C D,
+  Hom := λ F G, NaturalTransformation F G,
+  identity := λ F, IdentityNaturalTransformation F,
+  compose  := @vertical_composition_of_NaturalTransformations C D,
+
+  left_identity  := begin
+                     intros F G f,
+                     apply NaturalTransformations_componentwise_equal,
+                     intros,
+                     simp [ D^.left_identity ]
+                    end
+}