diff --git a/stage0/src/Init/Core.lean b/stage0/src/Init/Core.lean
index ce6fdb37d1..934bcb87c3 100644
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@@ -551,6 +551,9 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf
 | true,  x, y => x
 | false, x, y => y
 
+@[inline] def condEq {β : Sort u} (b : Bool) (h₁ : b = true → β) (h₂ : b = false → β) : β :=
+@Bool.casesOn (λ x => b = x → β) b h₂ h₁ rfl
+
 @[macroInline] def or : Bool → Bool → Bool
 | true,  _ => true
 | false, b => b
@@ -871,6 +874,19 @@ fun h => match s with
   | isTrue  h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁))
   | isFalse h₁ => h₁
 
+/-- Similar to `decide`, but uses an explicit instance -/
+@[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
+@decide p d
+
+theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
+@decideEqTrue _ d h
+
+theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
+@ofDecideEqTrue _ d h
+
+theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p :=
+@ofDecideEqFalse _ d h
+
 instance : Decidable True :=
 isTrue trivial
 
diff --git a/stage0/src/Init/Util.lean b/stage0/src/Init/Util.lean
index 5c0d06fbd4..7987b0142f 100644
--- a/stage0/src/Init/Util.lean
+++ b/stage0/src/Init/Util.lean
@@ -52,11 +52,12 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 k ()
 
 -- `withPtrEq` for `DecidableEq`
+
 @[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=
-let aux := withPtrEq a b (fun _ => @decide (a = b) (k ())) (fun h => @decideEqTrue _ (k ()) h);
-match aux, rfl : forall x (h : _ = x), _ with
-| true,  h => isTrue (@ofDecideEqTrue _ (k ()) h)
-| false, h => isFalse (@ofDecideEqFalse _ (k ()) h)
+let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsingEqTrue (k ()));
+condEq b
+  (fun h => isTrue (ofBoolUsingEqTrue h))
+  (fun h => isFalse (ofBoolUsingEqFalse h))
 
 @[implementedBy withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
diff --git a/stage0/src/library/compiler/csimp.cpp b/stage0/src/library/compiler/csimp.cpp
index 71b86c0434..6b064ccca4 100644
--- a/stage0/src/library/compiler/csimp.cpp
+++ b/stage0/src/library/compiler/csimp.cpp
@@ -1534,6 +1534,19 @@ class csimp_fn {
         return r;
     }
 
+    /* Applies `Bool.casesOn x false true` ==> `x`
+
+       This transformation is often applicable to code that goes back and forth between `Decidable` and `Bool`.
+       After `erase_irrelevant` both are `Bool`. */
+    optional<expr> is_identity_bool_cases_on (inductive_val const & I_val, buffer<expr> const & args) {
+        if (m_before_erasure) return none_expr();
+        if (args.size() == 3 && I_val.to_constant_val().get_name() == get_bool_name() &&
+            args[1] == mk_bool_false() && args[2] == mk_bool_true()) {
+            return some_expr(args[0]);
+        }
+        return none_expr();
+    }
+
     expr visit_cases(expr const & e, bool is_let_val) {
         buffer<expr> args;
         expr const & c = get_app_args(e, args);
@@ -1547,6 +1560,10 @@ class csimp_fn {
             major = nat_lit_to_constructor(major);
         }
 
+        if (optional<expr> r = is_identity_bool_cases_on(I_val, args)) {
+            return *r;
+        }
+
         if (is_constructor_app(env(), major)) {
             return reduce_cases_cnstr(args, I_val, major, is_let_val);
         } else if (!is_let_val) {
diff --git a/stage0/stdlib/Init/Core.c b/stage0/stdlib/Init/Core.c
index e190fd64ff..b203d97ad8 100644
--- a/stage0/stdlib/Init/Core.c
+++ b/stage0/stdlib/Init/Core.c
@@ -19,12 +19,14 @@ lean_object* l_strictAnd___boxed(lean_object*, lean_object*);
 lean_object* l_Prod_HasBeq(lean_object*, lean_object*);
 lean_object* lean_thunk_map(lean_object*, lean_object*);
 lean_object* l_Prod_DecidableEq___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_condEq___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_Subtype_sizeof(lean_object*);
 lean_object* l_Quotient_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
 uint8_t l_Prod_DecidableEq___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_inline(lean_object*);
 lean_object* l_Quotient_lift_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_condEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Function_swap___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Ne_Decidable(lean_object*);
 lean_object* l_Quotient_rec___boxed(lean_object*, lean_object*, lean_object*);
@@ -92,6 +94,7 @@ lean_object* l_Nat_HasOfNat___closed__1;
 lean_object* l_cond(lean_object*);
 lean_object* l_Decidable_byCases___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_recOnSubsingleton_u2082___at_Quotient_DecidableEq___spec__1(lean_object*, lean_object*);
+uint8_t l_toBoolUsing___rarg(uint8_t);
 lean_object* l_Eq_ndrecOn___rarg___boxed(lean_object*);
 lean_object* l_Quotient_mk(lean_object*, lean_object*);
 lean_object* l_Quotient_liftOn___rarg(lean_object*, lean_object*, lean_object*);
@@ -108,6 +111,7 @@ lean_object* l_decidableOfDecidableOfEq___rarg___boxed(lean_object*, lean_object
 lean_object* l___private_Init_Core_20__funSetoid(lean_object*, lean_object*);
 lean_object* l_EqvGen_Setoid(lean_object*, lean_object*);
 lean_object* l_Function_const___rarg(lean_object*, lean_object*);
+lean_object* l_toBoolUsing___rarg___boxed(lean_object*);
 lean_object* l_idDelta(lean_object*);
 uint8_t l_Or_Decidable___rarg(uint8_t, uint8_t);
 lean_object* l_cast___rarg___boxed(lean_object*);
@@ -214,6 +218,7 @@ lean_object* l_Fun_Inhabited___rarg(lean_object*, lean_object*);
 lean_object* l_and___boxed(lean_object*, lean_object*);
 lean_object* l_Eq_ndrec(lean_object*, lean_object*, lean_object*);
 lean_object* l_Sum_sizeof___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_toBoolUsing(lean_object*);
 lean_object* l_Subtype_Inhabited___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_ite___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_Eq_ndrec___rarg___boxed(lean_object*, lean_object*, lean_object*);
@@ -248,6 +253,7 @@ lean_object* l_inline___rarg___boxed(lean_object*);
 lean_object* l_Quotient_recOnSubsingleton(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Quot_liftOn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Decidable_recOnFalse___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_condEq(lean_object*);
 lean_object* l_PUnit_DecidableEq___boxed(lean_object*, lean_object*);
 lean_object* l_Decidable_recOnTrue___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_cast(lean_object*, lean_object*, lean_object*);
@@ -1505,6 +1511,43 @@ lean_dec(x_2);
 return x_5;
 }
 }
+lean_object* l_condEq___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (x_1 == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, lean_box(0));
+return x_4;
+}
+else
+{
+lean_object* x_5; 
+lean_dec(x_3);
+x_5 = lean_apply_1(x_2, lean_box(0));
+return x_5;
+}
+}
+}
+lean_object* l_condEq(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_condEq___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l_condEq___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; lean_object* x_5; 
+x_4 = lean_unbox(x_1);
+lean_dec(x_1);
+x_5 = l_condEq___rarg(x_4, x_2, x_3);
+return x_5;
+}
+}
 uint8_t l_or(uint8_t x_1, uint8_t x_2) {
 _start:
 {
@@ -1834,6 +1877,31 @@ x_2 = lean_alloc_closure((void*)(l_beqOfEq___rarg), 3, 0);
 return x_2;
 }
 }
+uint8_t l_toBoolUsing___rarg(uint8_t x_1) {
+_start:
+{
+return x_1;
+}
+}
+lean_object* l_toBoolUsing(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_toBoolUsing___rarg___boxed), 1, 0);
+return x_2;
+}
+}
+lean_object* l_toBoolUsing___rarg___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; uint8_t x_3; lean_object* x_4; 
+x_2 = lean_unbox(x_1);
+lean_dec(x_1);
+x_3 = l_toBoolUsing___rarg(x_2);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
 uint8_t _init_l_True_Decidable() {
 _start:
 {