diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean
index ec665b3d95..85ef5e885c 100644
--- a/src/Lean/Meta/Constructions.lean
+++ b/src/Lean/Meta/Constructions.lean
@@ -64,6 +64,7 @@ where
         safety      := DefinitionSafety.safe
         hints       := ReducibilityHints.abbrev
       }
+      setReducibleAttribute declName
 
   mkNoConfusionType : MetaM Unit := do
     let enumType := mkConst enumName
@@ -83,6 +84,7 @@ where
         safety      := DefinitionSafety.safe
         hints       := ReducibilityHints.abbrev
       }
+      setReducibleAttribute declName
 
   mkNoConfusion : MetaM Unit := do
     let enumType := mkConst enumName
@@ -105,6 +107,7 @@ where
         safety      := DefinitionSafety.safe
         hints       := ReducibilityHints.abbrev
       }
+      setReducibleAttribute declName
 
 def mkNoConfusion (declName : Name) : MetaM Unit := do
   if (← isEnumType declName) then
diff --git a/tests/lean/run/1016.lean b/tests/lean/run/1016.lean
new file mode 100644
index 0000000000..cb57cda9f9
--- /dev/null
+++ b/tests/lean/run/1016.lean
@@ -0,0 +1,5 @@
+inductive t | one | two
+
+example (h : False) : t.one = t.two := by
+  simp
+  contradiction