diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index cd82ac37bf..98b02fdd59 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2506,6 +2506,16 @@ theorem setWidth_eq_append {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) :
     omega
   · simp [hiv, getLsbD_ge x i (by omega)]
 
+theorem setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
+    x.setWidth w = (x.extractLsb' 0 w).cast (by omega) := by
+  rw [setWidth_eq_append_extractLsb']
+  ext i hi
+  simp only [getElem_cast, getElem_append]
+  by_cases hiv : i < v
+  · simp [hi]
+    omega
+  · simp [getLsbD_ge x i (by omega)]
+
 theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by
   ext i hi
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index ae7702d586..5ad98f855e 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -36,8 +36,6 @@ instance : ToExpr BVUnOp where
   toExpr x :=
     match x with
     | .not => mkConst ``BVUnOp.not
-    | .shiftLeftConst n => mkApp (mkConst ``BVUnOp.shiftLeftConst) (toExpr n)
-    | .shiftRightConst n => mkApp (mkConst ``BVUnOp.shiftRightConst) (toExpr n)
     | .rotateLeft n => mkApp (mkConst ``BVUnOp.rotateLeft) (toExpr n)
     | .rotateRight n => mkApp (mkConst ``BVUnOp.rotateRight) (toExpr n)
     | .arithShiftRightConst n => mkApp (mkConst ``BVUnOp.arithShiftRightConst) (toExpr n)
@@ -50,8 +48,6 @@ where
   go {w : Nat} : BVExpr w → Expr
   | .var idx => mkApp2 (mkConst ``BVExpr.var) (toExpr w) (toExpr idx)
   | .const val => mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
-  | .zeroExtend (w := oldWidth) val inner =>
-    mkApp3 (mkConst ``BVExpr.zeroExtend) (toExpr oldWidth) (toExpr val) (go inner)
   | .signExtend (w := oldWidth) val inner =>
     mkApp3 (mkConst ``BVExpr.signExtend) (toExpr oldWidth) (toExpr val) (go inner)
   | .bin lhs op rhs => mkApp4 (mkConst ``BVExpr.bin) (toExpr w) (go lhs) (toExpr op) (go rhs)
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
index 8c7ed98ca2..cc03b6ec1e 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -49,40 +49,24 @@ where
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
     | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeftConst
-          ``BVUnOp.shiftLeftConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
-      else
-        let_expr BitVec _ := β | return none
-        shiftReflection
-          distanceExpr
-          innerExpr
-          .shiftLeft
-          ``BVExpr.shiftLeft
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
+      if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
+      let_expr BitVec _ := β | return none
+      shiftReflection
+        distanceExpr
+        innerExpr
+        .shiftLeft
+        ``BVExpr.shiftLeft
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
     | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRightConst
-          ``BVUnOp.shiftRightConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
-      else
-        let_expr BitVec _ := β | return none
-        shiftReflection
-          distanceExpr
-          innerExpr
-          .shiftRight
-          ``BVExpr.shiftRight
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
+      if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
+      let_expr BitVec _ := β | return none
+      shiftReflection
+        distanceExpr
+        innerExpr
+        .shiftRight
+        ``BVExpr.shiftRight
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
     | BitVec.sshiftRight _ innerExpr distanceExpr =>
       let some distance ← getNatValue? distanceExpr | return none
       shiftConstLikeReflection
@@ -98,27 +82,6 @@ where
         .arithShiftRight
         ``BVExpr.arithShiftRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
-    | BitVec.zeroExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .zeroExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.zeroExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
-        let some innerProof ← inner.evalsAtAtoms | return none
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
     | BitVec.signExtend _ newWidthExpr innerExpr =>
       let some newWidth ← getNatValue? newWidthExpr | return none
       let some inner ← goOrAtom innerExpr | return none
@@ -131,7 +94,7 @@ where
           inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
+        -- This is safe as `signExtend_congr` holds definitionally if the arguments are defeq.
         let some innerProof ← inner.evalsAtAtoms | return none
         return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
           newWidthExpr
@@ -173,7 +136,7 @@ where
         inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
+        -- This is safe as `replicate_congr` holds definitionally if the arguments are defeq.
         let some innerProof ← inner.evalsAtAtoms | return none
         return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
           (toExpr n)
@@ -194,7 +157,7 @@ where
         inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
+        -- This is safe as `extract_congr` holds definitionally if the arguments are defeq.
         let some innerProof ← inner.evalsAtAtoms | return none
         return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
           startExpr
@@ -262,12 +225,6 @@ where
     let some distance ← getNatValue? distanceExpr | return none
     shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
 
-  shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
-      (shiftOpName : Name) (congrThm : Name) :
-      LemmaM (Option ReifiedBVExpr) := do
-    let some distance ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr | return none
-    shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
-
   shiftReflection (distanceExpr : Expr) (innerExpr : Expr)
       (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
       (congrThm : Name) :
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index 19694033d5..cea7db32f7 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -263,5 +263,112 @@ builtin_simproc [bv_normalize] bv_elim_shiftLeft_const ((_ : BitVec _) <<< (_ :
     let proof := mkApp4 (mkConst ``BitVec.shiftLeft_eq_zero) wExpr lhsExpr rhsExpr h
     return .done { expr := expr, proof? := some proof }
 
+builtin_simproc [bv_normalize] bv_concat_extract
+    ((HAppend.hAppend (α := BitVec (no_index _)) (β := BitVec (no_index _)) (γ := BitVec (no_index _))
+        (BitVec.extractLsb' _ _ _)
+        (BitVec.extractLsb' _ _ _)))
+    := fun e => do
+  let_expr HAppend.hAppend _ _ _ _ lhsExpr rhsExpr := e | return .continue
+  let_expr BitVec.extractLsb' wExpr lstartExpr llenExpr lhsVal := lhsExpr | return .continue
+  let some lstart ← getNatValue? lstartExpr | return .continue
+  let some llen ← getNatValue? llenExpr | return .continue
+  let_expr BitVec.extractLsb' _ rstartExpr rlenExpr rhsVal := rhsExpr | return .continue
+  let some rstart ← getNatValue? rstartExpr | return .continue
+  let some rlen ← getNatValue? rlenExpr | return .continue
+  if lhsVal != rhsVal then return .continue
+  if lstart != rstart + rlen then return .continue
+  let newLenExpr := toExpr (llen + rlen)
+  let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr rstartExpr newLenExpr lhsVal
+  let expr := mkApp4 (mkConst ``BitVec.cast) newLenExpr newLenExpr (← mkEqRefl newLenExpr) extract
+  let proof :=
+    mkApp7
+      (mkConst ``BitVec.extractLsb'_append_extractLsb'_eq_extractLsb')
+      wExpr
+      lstartExpr
+      rstartExpr
+      rlenExpr
+      llenExpr
+      lhsVal
+      (← mkEqRefl lstartExpr)
+  return .visit { expr := expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_concat_not_extract
+    ((HAppend.hAppend (α := BitVec (no_index _)) (β := BitVec (no_index _)) (γ := BitVec (no_index _))
+        (Complement.complement (α := BitVec (no_index _)) (BitVec.extractLsb' _ _ _))
+        (Complement.complement (α := BitVec (no_index _)) (BitVec.extractLsb' _ _ _))))
+    := fun e => do
+  let_expr HAppend.hAppend _ _ _ _ lhsExpr rhsExpr := e | return .continue
+  let_expr Complement.complement _ _ lhsExpr := lhsExpr | return .continue
+  let_expr Complement.complement _ _ rhsExpr := rhsExpr | return .continue
+  let_expr BitVec.extractLsb' wExpr lstartExpr llenExpr lhsVal := lhsExpr | return .continue
+  let some lstart ← getNatValue? lstartExpr | return .continue
+  let some llen ← getNatValue? llenExpr | return .continue
+  let_expr BitVec.extractLsb' _ rstartExpr rlenExpr rhsVal := rhsExpr | return .continue
+  let some rstart ← getNatValue? rstartExpr | return .continue
+  let some rlen ← getNatValue? rlenExpr | return .continue
+  if lhsVal != rhsVal then return .continue
+  if lstart != rstart + rlen then return .continue
+  let newLenExpr := toExpr (llen + rlen)
+  let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr rstartExpr newLenExpr lhsVal
+  let not ← mkAppM ``Complement.complement #[extract]
+  let expr := mkApp4 (mkConst ``BitVec.cast) newLenExpr newLenExpr (← mkEqRefl newLenExpr) not
+  let proof :=
+    mkApp7
+      (mkConst ``BitVec.not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb')
+      wExpr
+      lstartExpr
+      rstartExpr
+      rlenExpr
+      llenExpr
+      lhsVal
+      (← mkEqRefl lstartExpr)
+  return .visit { expr := expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_elim_setWidth (BitVec.setWidth _ _) := fun e => do
+  let_expr BitVec.setWidth oldWidthExpr newWidthExpr targetExpr := e | return .continue
+  let some oldWidth ← getNatValue? oldWidthExpr | return .continue
+  let some newWidth ← getNatValue? newWidthExpr | return .continue
+  if newWidth ≤ oldWidth then
+    let extract :=
+      mkApp4
+        (mkConst ``BitVec.extractLsb')
+        oldWidthExpr
+        (toExpr 0)
+        newWidthExpr
+        targetExpr
+    let expr :=
+      mkApp4
+        (mkConst ``BitVec.cast)
+        newWidthExpr
+        newWidthExpr
+        (← mkEqRefl newWidthExpr)
+        extract
+    let proof :=
+      mkApp4
+        (mkConst ``BitVec.setWidth_eq_extractLsb')
+        oldWidthExpr
+        targetExpr
+        newWidthExpr
+        (← mkDecideProof (← mkLe newWidthExpr oldWidthExpr))
+    return .visit { expr := expr, proof? := some proof }
+  else
+    let lhs := toExpr 0#(newWidth - oldWidth)
+    let concat ← mkAppM ``HAppend.hAppend #[lhs ,targetExpr]
+    let expr :=
+      mkApp4
+        (mkConst ``BitVec.cast)
+        newWidthExpr
+        newWidthExpr
+        (← mkEqRefl newWidthExpr)
+        concat
+    let proof :=
+      mkApp4
+        (mkConst ``BitVec.setWidth_eq_append)
+        oldWidthExpr
+        targetExpr
+        newWidthExpr
+        (← mkDecideProof (← mkLe oldWidthExpr newWidthExpr))
+    return .visit { expr := expr, proof? := some proof }
+
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index 28e1eb9955..8febb0724c 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -119,22 +119,6 @@ inductive BVUnOp where
   -/
   | not
   /--
-  Shifting left by a constant value.
-
-  This operation has a dedicated constant representation as shiftLeft can take `Nat` as a shift amount.
-  We can obviously not bitblast a `Nat` but still want to support the case where the user shifts by a
-  constant `Nat` value.
-  -/
-  | shiftLeftConst (n : Nat)
-  /--
-  Shifting right by a constant value.
-
-  This operation has a dedicated constant representation as shiftRight can take `Nat` as a shift amount.
-  We can obviously not bitblast a `Nat` but still want to support the case where the user shifts by a
-  constant `Nat` value.
-  -/
-  | shiftRightConst (n : Nat)
-  /--
   Rotating left by a constant value.
   -/
   | rotateLeft (n : Nat)
@@ -155,8 +139,6 @@ namespace BVUnOp
 
 def toString : BVUnOp → String
   | not => "~"
-  | shiftLeftConst n => s!"<< {n}"
-  | shiftRightConst n => s!">> {n}"
   | rotateLeft n => s!"rotL {n}"
   | rotateRight n => s!"rotR {n}"
   | arithShiftRightConst n => s!">>a {n}"
@@ -168,22 +150,12 @@ The semantics for `BVUnOp`.
 -/
 def eval : BVUnOp → (BitVec w → BitVec w)
   | not => (~~~ ·)
-  | shiftLeftConst n => (· <<< n)
-  | shiftRightConst n => (· >>> n)
   | rotateLeft n => (BitVec.rotateLeft · n)
   | rotateRight n => (BitVec.rotateRight · n)
   | arithShiftRightConst n => (BitVec.sshiftRight · n)
 
 @[simp] theorem eval_not : eval .not = ((~~~ ·) : BitVec w → BitVec w) := by rfl
 
-@[simp]
-theorem eval_shiftLeftConst : eval (shiftLeftConst n) = ((· <<< n) : BitVec w → BitVec w) := by
-  rfl
-
-@[simp]
-theorem eval_shiftRightConst : eval (shiftRightConst n) = ((· >>> n) : BitVec w → BitVec w) := by
-  rfl
-
 @[simp]
 theorem eval_rotateLeft : eval (rotateLeft n) = ((BitVec.rotateLeft · n) : BitVec w → BitVec w) := by
   rfl
@@ -211,10 +183,6 @@ inductive BVExpr : Nat → Type where
   -/
   | const (val : BitVec w) : BVExpr w
   /--
-  zero extend a `BitVec` by some constant amount.
-  -/
-  | zeroExtend (v : Nat) (expr : BVExpr w) : BVExpr v
-  /--
   Extract a slice from a `BitVec`.
   -/
   | extract (start len : Nat) (expr : BVExpr w) : BVExpr len
@@ -256,7 +224,6 @@ namespace BVExpr
 def toString : BVExpr w → String
   | .var idx => s!"var{idx}"
   | .const val => ToString.toString val
-  | .zeroExtend v expr => s!"(zext {v} {expr.toString})"
   | .extract start len expr => s!"{expr.toString}[{start}, {len}]"
   | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
   | .un op operand => s!"({op.toString} {toString operand})"
@@ -303,7 +270,6 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
     else
       packedBv.bv.truncate w
   | .const val => val
-  | .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
   | .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
   | .bin lhs op rhs => op.eval (eval assign lhs) (eval assign rhs)
   | .un op operand => op.eval (eval assign operand)
@@ -326,10 +292,6 @@ theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.tru
 @[simp]
 theorem eval_const : eval assign (.const val) = val := by rfl
 
-@[simp]
-theorem eval_zeroExtend : eval assign (.zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr) := by
-  rfl
-
 @[simp]
 theorem eval_extract : eval assign (.extract start len expr) = BitVec.extractLsb' start len (eval assign expr) := by
   rfl
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
index 6d5d0e7f2d..2d1b1dea44 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -11,7 +11,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
@@ -45,14 +44,6 @@ where
     | .const val =>
       let res := bitblast.blastConst aig val
       ⟨res, AIG.LawfulVecOperator.le_size (f := bitblast.blastConst) ..⟩
-    | .zeroExtend (w := w) v inner =>
-      let ⟨⟨aig, evec⟩, haig⟩ := go aig inner
-      let res := bitblast.blastZeroExtend aig ⟨w, evec⟩
-      have := by
-        apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastZeroExtend)
-        dsimp only at haig
-        assumption
-      ⟨res, this⟩
     | .signExtend (w := w) v inner =>
       let ⟨⟨aig, evec⟩, haig⟩ := go aig inner
       let res := bitblast.blastSignExtend aig ⟨w, evec⟩
@@ -127,20 +118,6 @@ where
             dsimp only at heaig
             omega
           ⟨res, this⟩
-      | .shiftLeftConst distance =>
-        let res := bitblast.blastShiftLeftConst eaig ⟨evec, distance⟩
-        have := by
-          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastShiftLeftConst)
-          dsimp only at heaig
-          assumption
-        ⟨res, this⟩
-      | .shiftRightConst distance =>
-        let res := bitblast.blastShiftRightConst eaig ⟨evec, distance⟩
-        have := by
-          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastShiftRightConst)
-          dsimp only at heaig
-          assumption
-        ⟨res, this⟩
       | .rotateLeft distance =>
         let res := bitblast.blastRotateLeft eaig ⟨evec, distance⟩
         have := by
@@ -251,19 +228,13 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
         apply Nat.le_trans <;> assumption
   | un op expr ih =>
     match op with
-    | .not | .shiftLeftConst .. | .shiftRightConst .. | .rotateLeft .. | .rotateRight ..
+    | .not | .rotateLeft .. | .rotateRight ..
     | .arithShiftRightConst .. =>
       dsimp only [go]
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [ih]
       have := (go aig expr).property
       omega
-  | zeroExtend w inner ih =>
-    dsimp only [go]
-    rw [AIG.LawfulVecOperator.decl_eq (f := blastZeroExtend)]
-    rw [ih]
-    have := (go aig inner).property
-    omega
   | signExtend w inner ih =>
     dsimp only [go]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastSignExtend)]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index c48f89973b..6c1907fce9 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -11,7 +11,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Not
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
@@ -67,11 +66,6 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp [go, denote_blastConst]
   | var =>
     simp [go, hidx, denote_blastVar]
-  | zeroExtend v inner ih =>
-    simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
-      eval_zeroExtend, BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and,
-      Bool.and_iff_right_iff_imp, decide_eq_true_eq]
-    apply BitVec.lt_of_getLsbD
   | append lhs rhs lih rih =>
     rename_i lw rw
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
@@ -229,16 +223,6 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
   | un op expr ih =>
     cases op with
     | not => simp [go, ih, hidx]
-    | shiftLeftConst i =>
-      rename_i w
-      simp [go, ih, hidx, show idx - i < w by omega]
-    | shiftRightConst =>
-      simp only [go, denote_blastShiftRightConst, ih, dite_eq_ite, Bool.if_false_right, eval_un,
-        BVUnOp.eval_shiftRightConst, BitVec.getLsbD_ushiftRight, Bool.and_iff_right_iff_imp,
-        decide_eq_true_eq]
-      intro h
-      apply BitVec.lt_of_getLsbD
-      assumption
     | rotateLeft => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
     | rotateRight => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
     | arithShiftRightConst n =>
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 5e8d98f8fc..58da852033 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -37,9 +37,8 @@ theorem BitVec.gt_ult (x y : BitVec w) : x > y ↔ (y.ult x = true) := by
 theorem BitVec.ge_ule (x y : BitVec w) : x ≥ y ↔ ((!x.ult y) = true) := by
   simp [BitVec.le_ult]
 
-@[bv_normalize]
-theorem BitVec.truncate_eq_zeroExtend (x : BitVec w) : x.truncate n = x.zeroExtend n := by
-  rfl
+attribute [bv_normalize] BitVec.zeroExtend_eq_setWidth
+attribute [bv_normalize] BitVec.truncate_eq_setWidth
 
 attribute [bv_normalize] BitVec.extractLsb
 attribute [bv_normalize] BitVec.msb_eq_getLsbD_last
@@ -151,8 +150,6 @@ section Constant
 
 attribute [bv_normalize] BitVec.add_zero
 attribute [bv_normalize] BitVec.zero_add
-attribute [bv_normalize] BitVec.setWidth_eq
-attribute [bv_normalize] BitVec.setWidth_zero
 attribute [bv_normalize] BitVec.getLsbD_zero
 attribute [bv_normalize] BitVec.getLsbD_zero_length
 attribute [bv_normalize] BitVec.getLsbD_concat_zero
@@ -419,5 +416,24 @@ theorem BitVec.and_const_left' :
 theorem BitVec.and_const_right' {a : BitVec w} :
     (a &&& BitVec.ofNat w b) &&& BitVec.ofNat w c = (BitVec.ofNat w b &&& BitVec.ofNat w c) &&& a := by
   ac_rfl
+
+-- Explicit no_index so this theorem works in the presence of constant folding if w1/w2/w3 are fixed
+@[bv_normalize]
+theorem BitVec.append_const_left {c : BitVec w3} :
+    HAppend.hAppend (β := BitVec (no_index _)) (γ := BitVec (no_index _))
+      (BitVec.ofNat w1 a)
+      (HAppend.hAppend (γ := BitVec (no_index _)) (BitVec.ofNat w2 b) c)
+    = ((BitVec.ofNat w1 a ++ BitVec.ofNat w2 b) ++ c).cast (Nat.add_assoc ..) := by
+  rw [BitVec.append_assoc]
+  simp
+
+@[bv_normalize]
+theorem BitVec.append_const_right {a : BitVec w1} :
+    HAppend.hAppend (α := BitVec (no_index _)) (γ := BitVec (no_index _))
+      (HAppend.hAppend (γ := BitVec (no_index _)) a (BitVec.ofNat w2 b))
+      (BitVec.ofNat w3 c)
+    = (a ++ (BitVec.ofNat w2 b ++ BitVec.ofNat w3 c)).cast (Eq.symm <| Nat.add_assoc ..) := by
+  rw [BitVec.append_assoc]
+
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index 070d10aa9f..8c4671c5a1 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -36,19 +36,11 @@ theorem xor_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2
 theorem not_congr (w : Nat) (x x' : BitVec w) (h : x = x') : ~~~x' = ~~~x := by
   simp[*]
 
-theorem shiftLeftNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
-    x' <<< n = x <<< n := by
-  simp[*]
-
 theorem shiftLeft_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
     (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
     lhs <<< rhs = lhs' <<< rhs' := by
   simp[*]
 
-theorem shiftRightNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
-    x' >>> n = x >>> n := by
-  simp[*]
-
 theorem shiftRight_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
     (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
     lhs >>> rhs = lhs' >>> rhs' := by
@@ -67,10 +59,6 @@ theorem add_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2
     lhs' + rhs' = lhs + rhs := by
   simp[*]
 
-theorem zeroExtend_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
-    BitVec.zeroExtend n x' = BitVec.zeroExtend n x := by
-  simp[*]
-
 theorem signExtend_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
     BitVec.signExtend n x' = BitVec.signExtend n x := by
   simp[*]
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 4222f8c54e..8dc35c0437 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -30,8 +30,6 @@ example (a b : Bool) : ((a = true) ↔ (b = true)) ↔ (a == b) := by bv_normali
 example {x : BitVec 16} : 0#16 + x = x := by bv_normalize
 example {x : BitVec 16} : x + 0#16 = x := by bv_normalize
 example {x : BitVec 16} : x.setWidth 16 = x := by bv_normalize
-example : (0#w).setWidth 32 = 0#32 := by bv_normalize
-example : (0#w).getLsbD i = false := by bv_normalize
 example {x : BitVec 0} : x.getLsbD i = false := by bv_normalize
 example {x : BitVec 16} {b : Bool} : (x.concat b).getLsbD 0 = b := by bv_normalize
 example {x : BitVec 16} : 1 * x = x := by bv_normalize
@@ -573,6 +571,18 @@ example {x : BitVec 8} : (x &&& 10) &&& 2 = 2 &&& x := by bv_normalize
 example {x : BitVec 8} : 2 &&& (x &&& 10) = 2 &&& x := by bv_normalize
 example {x : BitVec 8} : 2 &&& (10 &&& x) = 2 &&& x := by bv_normalize
 
+-- BV_CONCAT_CONST
+example {x : BitVec 8} : 8#4 ++ (4#4 ++ x) = 132#8 ++ x := by bv_normalize
+example {x : BitVec 8} : (x ++ 4#4) ++ 8#4 = x ++ 72#8 := by bv_normalize
+
+-- BV_CONCAT_EXTRACT
+example {x : BitVec 8} : x.extractLsb' 3 5 ++ x.extractLsb' 1 2 = x.extractLsb' 1 7 := by
+  bv_normalize
+
+example {x : BitVec 8} :
+    (~~~x.extractLsb' 3 5) ++ (~~~x.extractLsb' 1 2) = ~~~x.extractLsb' 1 7 := by
+  bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by