diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index aad29c957a..6c420af4ba 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/definitional/cases_on.h"
 #include "library/definitional/util.h"
 #include "library/definitional/projection.h"
+#include "library/definitional/no_confusion.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/decl_cmds.h"
@@ -640,6 +641,19 @@ struct structure_cmd_fn {
         }
     }
 
+    void add_rec_on_alias(name const & n) {
+        bool opaque = false;
+        name rec_on_name(m_name, "rec_on");
+        declaration rec_on_decl = m_env.get(rec_on_name);
+        declaration new_decl = mk_definition(m_env, n, rec_on_decl.get_univ_params(),
+                                             rec_on_decl.get_type(), rec_on_decl.get_value(),
+                                             opaque);
+        m_env = module::add(m_env, check(m_env, new_decl));
+        m_env = set_reducible(m_env, n, reducible_status::On);
+        save_def_info(n);
+        add_alias(n);
+    }
+
     void declare_auxiliary() {
         m_env = mk_rec_on(m_env, m_name);
         m_env = mk_induction_on(m_env, m_name);
@@ -649,16 +663,8 @@ struct structure_cmd_fn {
         add_rec_alias(induction_on_name);
         save_def_info(rec_on_name);
         save_def_info(induction_on_name);
-        name destruct_name(m_name, "destruct");
-        bool opaque = false;
-        declaration rec_on_decl = m_env.get(rec_on_name);
-        declaration destruct_decl = mk_definition(m_env, destruct_name, rec_on_decl.get_univ_params(),
-                                                  rec_on_decl.get_type(), rec_on_decl.get_value(),
-                                                  opaque);
-        m_env = module::add(m_env, check(m_env, destruct_decl));
-        m_env = set_reducible(m_env, destruct_name, reducible_status::On);
-        save_def_info(destruct_name);
-        add_alias(destruct_name);
+        add_rec_on_alias(name(m_name, "destruct"));
+        add_rec_on_alias(name(m_name, "cases_on"));
     }
 
     void get_parent_names(buffer<name> & parent_names) {
@@ -797,6 +803,15 @@ struct structure_cmd_fn {
         }
     }
 
+    void declare_no_confustion() {
+        if (!has_eq_decls(m_env) || !has_heq_decls(m_env))
+            return;
+        m_env = mk_no_confusion(m_env, m_name);
+        name no_confusion_name(m_name, "no_confusion");
+        save_def_info(no_confusion_name);
+        add_alias(no_confusion_name);
+    }
+
     environment operator()() {
         process_header();
         if (m_p.curr_is_token(get_assign_tk())) {
@@ -831,6 +846,7 @@ struct structure_cmd_fn {
         declare_coercions();
         declare_eta();
         declare_proj_over_mk();
+        declare_no_confustion();
         return m_env;
     }
 };
diff --git a/tests/lean/run/sigma_no_confusion.lean b/tests/lean/run/sigma_no_confusion.lean
index e346c454ff..234517ac35 100644
--- a/tests/lean/run/sigma_no_confusion.lean
+++ b/tests/lean/run/sigma_no_confusion.lean
@@ -1,6 +1,7 @@
 import data.sigma tools.tactic
 
 namespace sigma
+  namespace manual
   definition no_confusion_type {A : Type} {B : A → Type} (P : Type) (v₁ v₂ : sigma B) : Type :=
   rec_on v₁
     (λ (a₁ : A) (b₁ : B a₁), rec_on v₂
@@ -14,14 +15,14 @@ namespace sigma
         (λ (a₁ : A) (b₁ : B a₁) (h : Π (eq₁ : a₁ = a₁), eq.rec_on eq₁ b₁ = b₁ → P),
            h rfl rfl),
     eq.rec_on H₁₂ aux H₁₂
+ end manual
 
  theorem sigma.mk.inj_1 {A : Type} {B : A → Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (Heq : dpair a₁ b₁ = dpair a₂ b₂) : a₁ = a₂ :=
  begin
    apply (no_confusion Heq), intros, assumption
  end
 
- theorem sigma.mk.inj_2 {A : Type} {B : A → Type} (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂) (Heq : dpair a₁ b₁ = dpair a₂ b₂) :
-   eq.rec_on (sigma.mk.inj_1 Heq) b₁ = b₂ :=
+ theorem sigma.mk.inj_2 {A : Type} {B : A → Type} (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂) (Heq : dpair a₁ b₁ = dpair a₂ b₂) : b₁ == b₂ :=
  begin
    apply (no_confusion Heq), intros, eassumption
  end