From 228a99af7eeedc51ab649113c6d2b3fdb18b9631 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Jun 2015 19:51:28 -0700
Subject: [PATCH] feat(library/data/subtype): cleanup proof

---
 library/data/subtype.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index ae7e5229d..14a807e59 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -3,7 +3,6 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Jeremy Avigad
 -/
-
 open decidable
 
 set_option structure.proj_mk_thm true
@@ -30,9 +29,8 @@ namespace subtype
 
   protected definition has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂)
   | (tag v₁ p₁) (tag v₂ p₂) :=
-    begin
-      apply (@by_cases (v₁ = v₂)),
-        {intro e, revert p₁, rewrite e, intro p₁, left, congruence},
-        {intro n, right, intro h, injection h, contradiction}
+    match H v₁ v₂ with
+    | inl veq := begin left, substvars end
+    | inr vne := begin right, intro h, injection h, contradiction end
     end
 end subtype