fix: mark auxiliary noConfusion declarations for enumeration types as [reducible]

closes #1016

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

tests/lean/run/1016.lean

@@ -0,0 +1,5 @@
+inductive t | one | two
+
+example (h : False) : t.one = t.two := by
+  simp
+  contradiction