chore: update stage0

Without this change, we would not inline anything inside
let x_42 := casesOn x_3 fun .. => ... here ...

src/Init/Coe.lean

@@ -290,7 +290,7 @@ syntax:1024 (name := coeNotation) "↑" term:1024 : term
 /-! # Basic instances -/
 
 instance boolToProp : Coe Bool Prop where
-  coe b := Eq b true
+  coe := Bool.asProp
 
 instance boolToSort : CoeSort Bool Prop where
   coe b := b

src/Init/Core.lean

@@ -598,6 +598,10 @@ theorem Bool.of_not_eq_false : {b : Bool} → ¬ (b = false) → b = true
   | true,  _ => rfl
   | false, h => absurd rfl h
 
+theorem Bool.of_not_asProp : ¬ b.asProp → b = false := of_not_eq_true
+
+theorem Bool.of_asProp : b.asProp → b = true := id
+
 theorem ne_of_beq_false [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b := by
   intro h'; subst h'; have : true = false := Eq.trans LawfulBEq.rfl.symm h; contradiction
 

src/Init/Data/Array/DecidableEq.lean

@@ -31,14 +31,14 @@ theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y
    have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
    exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
 
-theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by
+theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i := by
   unfold Array.isEqvAux
   split
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by _ => a.size - i
 
-theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
+theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) := by
   simp [isEqv, isEqvAux_self]
 
 instance [DecidableEq α] : DecidableEq (Array α) :=

src/Init/Data/List/Basic.lean

@@ -331,9 +331,7 @@ def replace [BEq α] : List α → α → α → List α
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match a == b with
-    | true  => true
-    | false => elem a bs
+  | b::bs => a == b || elem a bs
 
 /-- `notElem a l` is `!(elem a l)`. -/
 def notElem [BEq α] (a : α) (as : List α) : Bool :=
@@ -356,22 +354,21 @@ inductive Mem (a : α) : List α → Prop
 instance : Membership α (List α) where
   mem := Mem
 
-theorem mem_of_elem_eq_true [DecidableEq α] {a : α} {as : List α} : elem a as = true → a ∈ as := by
-  match as with
-  | [] => simp [elem]
-  | a'::as =>
-    simp [elem]
-    split
-    next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head
-    next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)
+theorem elem_iff_mem [DecidableEq α] {a : α} {as : List α} : elem a as ↔ a ∈ as := by
+  show _ ↔ Mem a as
+  have not_mem_nil : ∀ {a : α}, ¬ Mem a nil := by intro _ h; cases h
+  have mem_cons_iff : ∀ {a b : α} {bs}, Mem a (b::bs) ↔ (a = b ∨ Mem a bs) := by
+    intros; constructor <;> intro h <;> cases h <;> simp [*, Mem.head, Mem.tail]
+  induction as <;> simp [elem, *]
 
-theorem elem_eq_true_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as = true := by
-  induction h with
-  | head _ => simp [elem]
-  | tail _ _ ih => simp [elem]; split; rfl; assumption
+theorem mem_of_elem [DecidableEq α] {a : α} {as : List α} : elem a as → a ∈ as :=
+  elem_iff_mem.1
+
+theorem elem_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as :=
+  elem_iff_mem.2 h
 
 instance [DecidableEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
+  decidable_of_decidable_of_iff elem_iff_mem
 
 theorem mem_append_of_mem_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
   intro h

src/Init/Data/Nat/Basic.lean

@@ -89,26 +89,18 @@ attribute [simp] Nat.zero_le
 
 /-! # Helper Bool relation theorems -/
 
-@[simp] theorem beq_refl (a : Nat) : Nat.beq a a = true := by
+@[simp] theorem beq_refl (a : Nat) : (Nat.beq a a).asProp := by
   induction a with simp [Nat.beq]
   | succ a ih => simp [ih]
 
-@[simp] theorem beq_eq : (Nat.beq x y = true) = (x = y) := propext <| Iff.intro Nat.eq_of_beq_eq_true (fun h => h ▸ (Nat.beq_refl x))
-@[simp] theorem ble_eq : (Nat.ble x y = true) = (x ≤ y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
-@[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
+@[simp] theorem beq_eq : (Nat.beq x y).asProp = (x = y) := propext <| Iff.intro Nat.eq_of_beq (fun h => h ▸ (Nat.beq_refl x))
+@[simp] theorem ble_eq : (Nat.ble x y).asProp = (x ≤ y) := propext <| Iff.intro Nat.le_of_ble Nat.ble_of_le
+@[simp] theorem blt_eq : (Nat.blt x y).asProp = (x < y) := propext <| Iff.intro Nat.le_of_ble Nat.ble_of_le
 
 instance : LawfulBEq Nat where
-  eq_of_beq h := Nat.eq_of_beq_eq_true h
+  eq_of_beq h := Nat.eq_of_beq h
   rfl := by simp [BEq.beq]
 
-@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
-@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
-  propext <| Iff.intro
-    (fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
-    (fun h =>
-      have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
-      by simp [this])
-
 /-! # Nat.add theorems -/
 
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n

src/Init/Data/Nat/Linear.lean

@@ -274,11 +274,12 @@ def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
 attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
 attribute [local simp] Poly.mul Poly.mul.go
+attribute [local simp] cond_eq_ite
 
 theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (v : Var) (p : Poly) : (p.insertSorted k v).denote ctx = p.denote ctx + k * v.denote ctx := by
   match p with
   | [] => simp
-  | (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
+  | (k', v') :: p => by_cases h : v < v' <;> simp [h, denote_insertSorted]
 
 attribute [local simp] Poly.denote_insertSorted
 
@@ -328,22 +329,22 @@ theorem Poly.denote_fuse (ctx : Context) (p : Poly) : p.fuse.denote ctx = p.deno
     simp
     split
     case _ h => simp [← ih, h]
-    case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
+    case _ k' v' p' h => by_cases he : v = v' <;> simp_all [he, ← ih, h]
 
 attribute [local simp] Poly.denote_fuse
 
-theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
-  simp
-  by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
-  by_cases h : k == 1 <;> simp [h]; simp [eq_of_beq h]
-  induction p with
-  | nil  => simp
-  | cons kv m ih => cases kv with | _ k' v => simp [ih]
+theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx :=
+  match k with
+  | 0 | 1 => by simp
+  | k+2 => by
+    induction p with
+    | nil  => simp
+    | cons kv m ih => cases kv with | _ k' v =>
+      simp_all [ih, show k + 1 ≠ 0 from (nomatch ·), show k + 2 ≠ 0 from (nomatch ·)]
+      simp only [Nat.mul_left_comm]
 
-private theorem eq_of_not_blt_eq_true (h₁ : ¬ (Nat.blt x y = true)) (h₂ : ¬ (Nat.blt y x = true)) : x = y :=
-  have h₁ : ¬ x < y := fun h => h₁ (Nat.blt_eq.mpr h)
-  have h₂ : ¬ y < x := fun h => h₂ (Nat.blt_eq.mpr h)
-  Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
+private theorem eq_of_not_lt {x y : Nat} (hxy : ¬ x < y) (hyx : ¬ y < x) : x = y :=
+  Nat.le_antisymm (Nat.ge_of_not_lt hyx) (Nat.ge_of_not_lt hxy)
 
 attribute [local simp] Poly.denote_mul
 
@@ -355,27 +356,27 @@ theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
     simp
     split <;> simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
+    by_cases hltv : v₁ < v₂ <;> simp [hltv]
     · apply ih; simp [denote_eq] at h |-; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv]
       · apply ih; simp [denote_eq] at h |-; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
+      · cases eq_of_not_lt hltv hgtv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk]
         · apply ih
           simp [denote_eq] at h |-
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
           apply Eq.symm
           apply Nat.sub_eq_of_eq_add
           simp [h]
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk]
           · apply ih
             simp [denote_eq] at h |-
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
             apply Nat.sub_eq_of_eq_add
             simp [h]
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · cases eq_of_not_lt hltk hgtk
             apply ih
             simp [denote_eq] at h |-
             rw [← Nat.add_assoc, ← Nat.add_assoc] at h
@@ -389,26 +390,26 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
     simp at h
     split at h <;> simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
+    by_cases hltv : v₁ < v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv] at h
       · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
+      · cases eq_of_not_lt hltv hgtv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk] at h
         · have ih := ih (h := h); simp [denote_eq] at ih ⊢
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
           have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih.symm
           simp at ih
           rw [ih]
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk] at h
           · have ih := ih (h := h); simp [denote_eq] at ih ⊢
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
             have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih
             simp at ih
             rw [ih]
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · cases eq_of_not_lt hltk hgtk
             have ih := ih (h := h); simp [denote_eq] at ih ⊢
             rw [← Nat.add_assoc, ih, Nat.add_assoc]
 
@@ -434,26 +435,26 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
     simp
     split <;> simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
+    by_cases hltv : v₁ < v₂ <;> simp [hltv]
     · apply ih; simp [denote_le] at h |-; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv]
       · apply ih; simp [denote_le] at h |-; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
+      · have heqv : v₁ = v₂ := eq_of_not_lt hltv hgtv; subst heqv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk]
         · apply ih
           simp [denote_le] at h |-
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
           apply Nat.le_sub_of_add_le
           simp [h]
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk]
           · apply ih
             simp [denote_le] at h |-
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
             apply Nat.sub_le_of_le_add
             simp [h]
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_lt hltk hgtk; subst heqk
             apply ih
             simp [denote_le] at h |-
             rw [← Nat.add_assoc, ← Nat.add_assoc] at h
@@ -468,26 +469,26 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
     simp at h
     split at h <;> simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
+    by_cases hltv : v₁ < v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv] at h
       · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
+      · have heqv : v₁ = v₂ := eq_of_not_lt hltv hgtv; subst heqv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk] at h
         · have ih := ih (h := h); simp [denote_le] at ih ⊢
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
           have := Nat.add_le_of_le_sub (Nat.le_trans haux (Nat.le_add_left ..)) ih
           simp at this
           exact this
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk] at h
           · have ih := ih (h := h); simp [denote_le] at ih ⊢
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
             have := Nat.le_add_of_sub_le ih
             simp at this
             exact this
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_lt hltk hgtk; subst heqk
             have ih := ih (h := h); simp [denote_le] at ih ⊢
             have := Nat.add_le_add_right ih (k₁ * Var.denote ctx v₁)
             simp at this
@@ -512,10 +513,9 @@ theorem Poly.denote_combineAux (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) :
   | succ fuel ih =>
     split <;> simp
     rename_i k₁ v₁ p₁ k₂ v₂ p₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv, ih]
-    by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv, ih]
-    have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv
-    simp [heqv]
+    by_cases hltv : v₁ < v₂ <;> simp [hltv, ih]
+    by_cases hgtv : v₂ < v₁ <;> simp [hgtv, ih]
+    simp [eq_of_not_lt hgtv hltv]
 
 theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   simp [combine, denote_combineAux]
@@ -524,7 +524,7 @@ attribute [local simp] Poly.denote_combine
 
 theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
   induction e with
-  | num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
+  | num k => by_cases h : k = 0 <;> simp [toPoly, h, Var.denote]
   | var i => simp [toPoly]
   | add a b iha ihb => simp [toPoly, iha, ihb]
   | mulL k a ih => simp [toPoly, ih, -Poly.mul]
@@ -559,7 +559,7 @@ theorem ExprCnstr.toPoly_norm_eq (c : ExprCnstr) : c.toPoly.norm = c.toNormPoly
 theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
-  by_cases h : eq = true <;> simp [h]
+  by_cases h : eq <;> simp [h]
   · simp [Poly.denote_eq, Expr.toPoly]
   · simp [Poly.denote_le, Expr.toPoly]
 
@@ -568,7 +568,7 @@ attribute [local simp] ExprCnstr.denote_toPoly
 theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPoly.denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]
-  by_cases h : eq = true <;> simp [h]
+  by_cases h : eq <;> simp [h]
   · rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
   · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]
 
@@ -586,13 +586,9 @@ attribute [-simp] Nat.right_distrib Nat.left_distrib
 
 theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
-  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp; apply Nat.succ_ne_zero
-  have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
-  have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
-  have : (1 == (0 : Nat)) = false := rfl
-  have : (1 == (1 : Nat)) = true  := rfl
-  by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
-     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
+  have : k + 1 ≠ 0 := (nomatch ·)
+  by_cases he : eq <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
+     <;> by_cases hk : k = 0 <;> (try simp [hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
   · rw [h]
   · exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
@@ -606,7 +602,7 @@ theorem PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ :
   cases c₁; cases c₂; rename_i eq₁ lhs₁ rhs₁ eq₂ lhs₂ rhs₂
   simp [denote] at h₁ h₂
   simp [PolyCnstr.combine, denote]
-  by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] at h₁ h₂ |-
+  by_cases he₁ : eq₁ <;> by_cases he₂ : eq₂ <;> simp [he₁, he₂] at h₁ h₂ |-
   · rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
   · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
   · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
@@ -618,28 +614,28 @@ theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = so
   simp [isNum?]
   split
   next => intro h; injection h
-  next k v => by_cases h : v == fixedVar <;> simp [h]; intros; simp [Var.denote, eq_of_beq h]; assumption
+  next k v => by_cases h : v = fixedVar <;> simp [h]; intros; simp [Var.denote, h]; assumption
   next => intros; contradiction
 
-theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p = true) : p.denote ctx = 0 := by
+theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p) : p.denote ctx = 0 := by
   simp [isZero] at h
   split at h
   · simp
   · contradiction
 
-theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) : p.denote ctx > 0 := by
+theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p) : p.denote ctx > 0 := by
   match p with
   | [] => contradiction
   | (k, v) :: p =>
-    by_cases he : v == fixedVar <;> simp [he, isNonZero] at h ⊢
-    · simp [eq_of_beq he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
+    by_cases he : v = fixedVar <;> simp [he, isNonZero] at h ⊢
+    · simp [he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
     · have ih := of_isNonZero ctx h
       exact Nat.le_trans ih (Nat.le_add_right ..)
 
 theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by
   cases c; rename_i eq lhs rhs
   simp [isUnsat]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
+  by_cases he : eq <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
   · intro
       | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
       | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
@@ -652,7 +648,7 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa
 theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by
   cases c; rename_i eq lhs rhs
   simp [isValid]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
+  by_cases he : eq <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₁, h₂]
   · intro h
@@ -694,9 +690,9 @@ theorem Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : c
 
 theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx := by
   simp [monomialToExpr]
-  by_cases h : v == fixedVar <;> simp [h, Expr.denote]
-  · simp [eq_of_beq h, Var.denote]
-  · by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
+  by_cases h : v = fixedVar <;> simp [h, Expr.denote]
+  · simp [h, Var.denote]
+  · by_cases h : k = 1 <;> simp [h, Expr.denote]
 
 attribute [local simp] denote_monomialToExpr
 

src/Init/Data/Nat/SOM.lean

@@ -113,11 +113,11 @@ where
     induction fuel generalizing m₁ m₂ with
     | zero => simp! [append_denote]
     | succ _ ih =>
-      simp!
+      simp! [cond_eq_ite]
       split <;> simp!
       next v₁ m₁ v₂ m₂ =>
-        by_cases hlt : Nat.blt v₁ v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
-        by_cases hgt : Nat.blt v₂ v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]
+        by_cases hlt : v₁ < v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
+        by_cases hgt : v₂ < v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]
 
 theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   match p₁ with
@@ -135,11 +135,11 @@ where
       split <;> simp!
       next k₁ m₁ p₁ k₂ m₂ p₂ =>
         by_cases hlt : m₁ < m₂ <;> simp! [hlt, Nat.add_assoc, ih]
-        by_cases hgt : m₂ < m₁ <;> simp! [hgt, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, ih]
+        by_cases hgt : m₂ < m₁ <;> simp! [hgt, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, ih, cond_eq_ite]
         have : m₁ = m₂ := List.le_antisymm hgt hlt
         subst m₂
-        by_cases heq : k₁ + k₂ == 0 <;> simp! [heq, ih]
-        · simp [← Nat.add_assoc, ← Nat.right_distrib, eq_of_beq heq]
+        by_cases heq : k₁ + k₂ = 0 <;> simp! [heq, ih, if_pos, if_neg]
+        · simp [← Nat.add_assoc, ← Nat.right_distrib, heq]
         · simp [Nat.right_distrib, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
 
 theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (m : Mon) (p : Poly) : (p.insertSorted k m).denote ctx = p.denote ctx + k * m.denote ctx := by
@@ -171,8 +171,7 @@ where
 theorem Expr.toPoly_denote (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
   induction e with
   | num k =>
-    simp!; by_cases h : k == 0 <;> simp! [*]
-    simp [eq_of_beq h]
+    simp!; by_cases h : k = 0 <;> simp! [*, cond_eq_ite]
   | var v => simp!
   | add a b => simp! [Poly.add_denote, *]
   | mul a b => simp! [Poly.mul_denote, *]

src/Init/Prelude.lean

@@ -550,6 +550,10 @@ inductive Bool : Type where
 
 export Bool (false true)
 
+/-- Interprets a Boolean value as a proposition. -/
+def Bool.asProp (b : Bool) : Prop :=
+  Eq b true
+
 /--
 `Subtype p`, usually written as `{x : α // p x}`, is a type which
 represents all the elements `x : α` for which `p x` is true. It is structurally
@@ -844,6 +848,13 @@ theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide
   | isTrue  _  => rfl
   | isFalse h₁ => absurd rfl h₁
 
+theorem decide_asProp_of [Decidable p] : p → (decide p).asProp := decide_eq_true
+
+instance : Decidable (Bool.asProp b) :=
+  match b with
+  | true => isTrue rfl
+  | false => isFalse (nomatch ·)
+
 /-- Decidable equality for Bool -/
 @[inline] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
    match a, b with
@@ -1478,13 +1489,13 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
 instance : BEq Nat where
   beq := Nat.beq
 
-theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
+protected theorem Nat.eq_of_beq : {n m : Nat} → (beq n m).asProp → Eq n m
   | zero,   zero,   _ => rfl
   | zero,   succ _, h => Bool.noConfusion h
   | succ _, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
     have : Eq (beq n m) true := h
-    have : Eq n m := eq_of_beq_eq_true this
+    have : Eq n m := Nat.eq_of_beq this
     this ▸ rfl
 
 theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
@@ -1505,7 +1516,7 @@ here is the logical model.
 @[reducible, extern "lean_nat_dec_eq"]
 protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) :=
   match h:beq n m with
-  | true  => isTrue (eq_of_beq_eq_true h)
+  | true  => isTrue (Nat.eq_of_beq h)
   | false => isFalse (ne_of_beq_eq_false h)
 
 @[inline] instance : DecidableEq Nat := Nat.decEq
@@ -1649,30 +1660,30 @@ protected theorem Nat.lt_of_le_of_ne {n m : Nat} (h₁ : LE.le n m) (h₂ : Not
   | Or.inl h₃ => h₃
   | Or.inr h₃ => absurd (Nat.le_antisymm h₁ h₃) h₂
 
-theorem Nat.le_of_ble_eq_true (h : Eq (Nat.ble n m) true) : LE.le n m :=
+theorem Nat.le_of_ble (h : (Nat.ble n m).asProp) : LE.le n m :=
   match n, m with
   | 0,      _      => Nat.zero_le _
-  | succ _, succ _ => Nat.succ_le_succ (le_of_ble_eq_true h)
+  | succ _, succ _ => Nat.succ_le_succ (le_of_ble h)
 
-theorem Nat.ble_self_eq_true : (n : Nat) → Eq (Nat.ble n n) true
+theorem Nat.ble_self : (n : Nat) → (Nat.ble n n).asProp
   | 0      => rfl
-  | succ n => ble_self_eq_true n
+  | succ n => ble_self n
 
-theorem Nat.ble_succ_eq_true : {n m : Nat} → Eq (Nat.ble n m) true → Eq (Nat.ble n (succ m)) true
+theorem Nat.ble_succ : {n m : Nat} → (Nat.ble n m).asProp → (Nat.ble n (succ m)).asProp
   | 0,      _,      _ => rfl
-  | succ n, succ _, h => ble_succ_eq_true (n := n) h
+  | succ n, succ _, h => ble_succ (n := n) h
 
-theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
+theorem Nat.ble_of_le (h : LE.le n m) : (Nat.ble n m).asProp :=
   match h with
-  | Nat.le.refl   => Nat.ble_self_eq_true n
-  | Nat.le.step h => Nat.ble_succ_eq_true (ble_eq_true_of_le h)
+  | Nat.le.refl   => Nat.ble_self n
+  | Nat.le.step h => Nat.ble_succ (ble_of_le h)
 
-theorem Nat.not_le_of_not_ble_eq_true (h : Not (Eq (Nat.ble n m) true)) : Not (LE.le n m) :=
-  fun h' => absurd (Nat.ble_eq_true_of_le h') h
+theorem Nat.not_le_of_not_ble (h : Not (Nat.ble n m).asProp) : Not (LE.le n m) :=
+  fun h' => absurd (Nat.ble_of_le h') h
 
 @[extern "lean_nat_dec_le"]
 instance Nat.decLe (n m : @& Nat) : Decidable (LE.le n m) :=
-  dite (Eq (Nat.ble n m) true) (fun h => isTrue (Nat.le_of_ble_eq_true h)) (fun h => isFalse (Nat.not_le_of_not_ble_eq_true h))
+  dite (Nat.ble n m).asProp (fun h => isTrue (Nat.le_of_ble h)) (fun h => isFalse (Nat.not_le_of_not_ble h))
 
 @[extern "lean_nat_dec_lt"]
 instance Nat.decLt (n m : @& Nat) : Decidable (LT.lt n m) :=

src/Init/SimpLemmas.lean

@@ -127,16 +127,15 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
 @[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
 
-@[simp] theorem Bool.beq_to_eq (a b : Bool) :
+theorem Bool.beq_to_eq (a b : Bool) :
   (a == b) = (a = b) := by cases a <;> cases b <;> decide
-@[simp] theorem Bool.not_beq_to_not_eq (a b : Bool) :
+theorem Bool.not_beq_to_not_eq (a b : Bool) :
   (!(a == b)) = ¬(a = b) := by cases a <;> cases b <;> decide
 
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
 
 @[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true
-@[simp] theorem decide_not [h : Decidable p] : decide (¬ p) = !decide p := by cases h <;> rfl
 @[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
 
 @[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
@@ -144,6 +143,10 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
 
+theorem cond_eq_ite : cond c a b = ite c a b := by cases c <;> simp
+theorem cond_pos : c.asProp → cond c a b = a := by cases c <;> simp
+theorem cond_neg : ¬ c.asProp → cond c a b = b := by cases c <;> simp
+
 @[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl
 @[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
 
@@ -153,5 +156,21 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
   propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by simp [h]⟩
 
+@[simp] theorem Bool.asProp_decide [Decidable p] : (decide p).asProp = p := by simp [asProp]
+@[simp] theorem Bool.asProp_false : false.asProp = False := by simp [asProp]
+@[simp] theorem Bool.asProp_true : true.asProp = True := by simp [asProp]
+@[simp] theorem Bool.asProp_and : (b && c).asProp = (b ∧ c) := by simp [asProp]
+@[simp] theorem Bool.asProp_or : (b || c).asProp = (b ∨ c) := by simp [asProp]
+@[simp] theorem Bool.asProp_not : (!b).asProp = (¬ b) := by simp [asProp]
+@[simp] theorem Bool.asProp_beq [BEq α] [LawfulBEq α] (a b : α) : (a == b).asProp = (a = b) :=
+  propext ⟨eq_of_beq, (by subst ·; apply LawfulBEq.rfl)⟩
+
+theorem Bool.eq_of_asProp_eq {b c : Bool} : b.asProp = c.asProp → b = c := by
+  cases b <;> cases c <;> simp
+
+@[simp] theorem decide_asProp : decide (Bool.asProp b) = b := by cases b <;> simp
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True : decide True = true := rfl
+@[simp] theorem decide_and [Decidable p] [Decidable q] : decide (p ∧ q) = (decide p && decide q) := Bool.eq_of_asProp_eq (by simp)
+@[simp] theorem decide_or [Decidable p] [Decidable q] : decide (p ∨ q) = (decide p || decide q) := Bool.eq_of_asProp_eq (by simp)
+@[simp] theorem decide_not [Decidable p] : decide (¬ p) = !decide p := Bool.eq_of_asProp_eq (by simp)

src/Init/Util.lean

@@ -57,11 +57,11 @@ unsafe def ptrEqList : (as bs : List α) → Bool
   | _, _ => false
 
 set_option linter.unusedVariables.funArgs false in
-@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
+@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k ()) : Bool :=
   if ptrEq a b then true else k ()
 
 @[implemented_by withPtrEqUnsafe]
-def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool := k ()
+def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k ()) : Bool := k ()
 
 /-- `withPtrEq` for `DecidableEq` -/
 @[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -263,21 +263,14 @@ where
   else if let some (_, lhs, rhs) := type.ne? then
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'False'"
-    if rhs.isConstOf ``Bool.true then
-      return [(← mkAppM ``Bool.of_not_eq_true #[e], ← mkEq lhs (mkConst ``Bool.false))]
-    else if rhs.isConstOf ``Bool.false then
-      return [(← mkAppM ``Bool.of_not_eq_false #[e], ← mkEq lhs (mkConst ``Bool.true))]
     let type ← mkEq (← mkEq lhs rhs) (mkConst ``False)
     let e    ← mkEqFalse e
     return [(e, type)]
   else if let some p := type.not? then
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'False'"
-    if let some (_, lhs, rhs) := p.eq? then
-      if rhs.isConstOf ``Bool.true then
-        return [(← mkAppM ``Bool.of_not_eq_true #[e], ← mkEq lhs (mkConst ``Bool.false))]
-      else if rhs.isConstOf ``Bool.false then
-        return [(← mkAppM ``Bool.of_not_eq_false #[e], ← mkEq lhs (mkConst ``Bool.true))]
+    if let some b := p.asProp? then
+      return [(← mkAppM ``Bool.of_not_asProp #[e], ← mkEq b (mkConst ``false))]
     let type ← mkEq p (mkConst ``False)
     let e    ← mkEqFalse e
     return [(e, type)]
@@ -285,6 +278,10 @@ where
     let e₁ := mkProj ``And 0 e
     let e₂ := mkProj ``And 1 e
     return (← go e₁ type₁) ++ (← go e₂ type₂)
+  else if let some b := type.asProp? then
+    if inv then
+      throwError "invalid '←' modifier in rewrite rule to 'true'"
+    return [(← mkAppM ``Bool.of_asProp #[e], ← mkEq b (mkConst ``true))]
   else
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'True'"

src/Lean/Util/Recognizers.lean

@@ -63,6 +63,9 @@ namespace Expr
 @[inline] def and? (p : Expr) : Option (Expr × Expr) :=
   p.app2? ``And
 
+@[inline] def asProp? (p : Expr) : Option Expr :=
+  p.app1? ``Bool.asProp
+
 @[inline] def heq? (p : Expr) : Option (Expr × Expr × Expr × Expr) :=
   p.app4? ``HEq
 

src/library/compiler/csimp.cpp

@@ -1606,10 +1606,8 @@ class csimp_fn {
 
         if (is_constructor_app(env(), major)) {
             return reduce_cases_cnstr(args, I_val, major, is_let_val);
-        } else if (!is_let_val) {
-            return visit_cases_default(e);
         } else {
-            return e;
+            return visit_cases_default(e);
         }
     }