diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 39348d0349..744a08cbf4 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -274,7 +274,8 @@ struct structure_cmd_fn {
     */
     expr update_locals(expr new_tmp, buffer<expr> & locals) {
         for (unsigned i = 0; i < locals.size(); i++) {
-            expr new_local = mk_local(binding_name(new_tmp), binding_domain(new_tmp), binding_info(new_tmp));
+            expr new_local = mk_local(mlocal_name(locals[i]), binding_name(new_tmp), binding_domain(new_tmp),
+                                      binding_info(new_tmp));
             locals[i]      = new_local;
             new_tmp        = instantiate(binding_body(new_tmp), new_local);
         }
diff --git a/tests/lean/hott/443.hlean b/tests/lean/hott/443.hlean
new file mode 100644
index 0000000000..f9ab5b8f6e
--- /dev/null
+++ b/tests/lean/hott/443.hlean
@@ -0,0 +1,13 @@
+import algebra.group algebra.precategory.basic algebra.precategory.morphism
+
+open eq sigma unit precategory morphism path_algebra
+
+context
+  parameters {P₀ : Type} [P : precategory P₀]
+
+  structure my_structure := (a : P₀) (b : P₀) (f : @hom P₀ P a b)
+  include P
+
+  structure another_structure (X : my_structure) := (field1 : hom (my_structure.a X) (my_structure.a X))
+
+end