diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
index 1416e58716f7..01ce8224aadb 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -225,8 +225,8 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
-    if let some reflected ← SatAtBVLogical.of (mkFVar hyp) then
-      sats := sats.push reflected
+    if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
+      sats := (sats ++ lemmas).push reflected
     else
       unusedHypotheses := unusedHypotheses.insert hyp
   if h : sats.size = 0 then
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index 7a1395adfd14..13af0cd31e81 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -80,6 +80,7 @@ instance : ToExpr Gate where
     | .and => mkConst ``Gate.and
     | .xor => mkConst ``Gate.xor
     | .beq => mkConst ``Gate.beq
+    | .imp => mkConst ``Gate.imp
   toTypeExpr := mkConst ``Gate
 
 instance : ToExpr BVPred where
@@ -125,6 +126,76 @@ The reflection monad, used to track `BitVec` variables that we see as we travers
 -/
 abbrev M := StateRefT State MetaM
 
+/--
+A reified version of an `Expr` representing a `BVExpr`.
+-/
+structure ReifiedBVExpr where
+  width : Nat
+  /--
+  The reified expression.
+  -/
+  bvExpr : BVExpr width
+  /--
+  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
+  -/
+  evalsAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvExpr`.
+  -/
+  expr : Expr
+
+/--
+A reified version of an `Expr` representing a `BVPred`.
+-/
+structure ReifiedBVPred where
+  /--
+  The reified expression.
+  -/
+  bvPred : BVPred
+  /--
+  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
+  -/
+  evalsAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvPred`
+  -/
+  expr : Expr
+
+/--
+A reified version of an `Expr` representing a `BVLogicalExpr`.
+-/
+structure ReifiedBVLogical where
+  /--
+  The reified expression.
+  -/
+  bvExpr : BVLogicalExpr
+  /--
+  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
+  -/
+  evalsAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvExpr`
+  -/
+  expr : Expr
+
+/--
+A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
+-/
+structure SatAtBVLogical where
+  /--
+  The reified expression.
+  -/
+  bvExpr : BVLogicalExpr
+  /--
+  A proof that `bvExpr.eval atomsAssignment = true`.
+  -/
+  satAtAtoms : M Expr
+  /--
+  A cache for `toExpr bvExpr`
+  -/
+  expr : Expr
+
+
 namespace M
 
 /--
@@ -172,5 +243,34 @@ where
 
 end M
 
+/--
+The state of the lemma reflection monad.
+-/
+structure LemmaState where
+  /--
+  The list of top level lemmas that got created on the fly during reflection.
+  -/
+  lemmas : Array SatAtBVLogical := #[]
+
+/--
+The lemma reflection monad. It extends the usual reflection monad `M` by adding the ability to
+add additional top level lemmas on the fly.
+-/
+abbrev LemmaM := StateRefT LemmaState M
+
+namespace LemmaM
+
+def run (m : LemmaM α) (state : LemmaState := {}) : M (α × Array SatAtBVLogical) := do
+  let (res, state) ← StateRefT'.run m state
+  return (res, state.lemmas)
+
+/--
+Add another top level lemma.
+-/
+def addLemma (lemma : SatAtBVLogical) : LemmaM Unit := do
+  modify fun s => { s with lemmas := s.lemmas.push lemma }
+
+end LemmaM
+
 end Frontend
 end Lean.Elab.Tactic.BVDecide
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
index 64c2f9552de7..aeb0526e97ed 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
@@ -14,30 +14,14 @@ Provides the logic for reifying `BitVec` expressions.
 namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
 
-open Lean.Meta
 open Std.Tactic.BVDecide
-open Std.Tactic.BVDecide.Reflect.BitVec
-
-/--
-A reified version of an `Expr` representing a `BVExpr`.
--/
-structure ReifiedBVExpr where
-  width : Nat
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVExpr width
-  /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`.
-  -/
-  expr : Expr
+open Lean.Meta
 
 namespace ReifiedBVExpr
 
+/--
+Build `BVExpr.eval atoms expr` where `atoms` is the assignment stored in the monad.
+-/
 def mkEvalExpr (w : Nat) (expr : Expr) : M Expr := do
   return mkApp3 (mkConst ``BVExpr.eval) (toExpr w) (← M.atomsAssignment) expr
 
@@ -47,6 +31,9 @@ def mkBVRefl (w : Nat) (expr : Expr) : Expr :=
    (mkApp (mkConst ``BitVec) (toExpr w))
    expr
 
+/--
+Register `e` as an atom of width `width`.
+-/
 def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
   let ident ← M.lookup e width
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
@@ -55,6 +42,9 @@ def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
     return mkBVRefl width evalExpr
   return ⟨width, .var ident, proof, expr⟩
 
+/--
+Parse `expr` as a `Nat` or `BitVec` constant depending on `ty`.
+-/
 def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   match_expr ty with
   | Nat =>
@@ -75,301 +65,15 @@ def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
   return some atom
 
 /--
-Reify an `Expr` that's a constant-width `BitVec`.
-Unless this function is called on something that is not a constant-width `BitVec` it is always
-going to return `some`.
+Build a reified version of the constant `val`.
 -/
-partial def of (x : Expr) : M (Option ReifiedBVExpr) := do
-  goOrAtom x
-where
-  /--
-  Reify `x`, returns `none` if the reification procedure failed.
-  -/
-  go (x : Expr) : M (Option ReifiedBVExpr) := do
-    match_expr x with
-    | BitVec.ofNat _ _ => goBvLit x
-    | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
-    | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
-    | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
-    | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
-    | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
-    | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
-    | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | BitVec.sdiv _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
-    | Complement.complement _ _ innerExpr =>
-      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
-    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeftConst
-          ``BVUnOp.shiftLeftConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeft
-          ``BVExpr.shiftLeft
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
-    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRightConst
-          ``BVUnOp.shiftRightConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
-      else
-        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
-        distance
-        innerExpr
-        .arithShiftRightConst
-        ``BVUnOp.arithShiftRightConst
-        ``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 ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        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
-      let bvExpr := .signExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.signExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
-      let some lhs ← goOrAtom lhsExpr | return none
-      let some rhs ← goOrAtom rhsExpr | return none
-      let bvExpr := .append lhs.bvExpr rhs.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.append)
-        (toExpr lhs.width)
-        (toExpr rhs.width)
-        lhs.expr rhs.expr
-      let proof := do
-        let lhsEval ← mkEvalExpr lhs.width lhs.expr
-        let lhsProof ← lhs.evalsAtAtoms
-        let rhsProof ← rhs.evalsAtAtoms
-        let rhsEval ← mkEvalExpr rhs.width rhs.expr
-        return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
-          (toExpr lhs.width) (toExpr rhs.width)
-          lhsExpr lhsEval
-          rhsExpr rhsEval
-          lhsProof rhsProof
-      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
-    | BitVec.replicate _ nExpr innerExpr =>
-      let some inner ← goOrAtom innerExpr | return none
-      let some n ← getNatValue? nExpr | return none
-      let bvExpr := .replicate n inner.bvExpr
-      let expr := mkApp3 (mkConst ``BVExpr.replicate)
-        (toExpr inner.width)
-        (toExpr n)
-        inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
-          (toExpr n)
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨inner.width * n, bvExpr, proof, expr⟩
-    | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
-      let some start ← getNatValue? startExpr | return none
-      let some len ← getNatValue? lenExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .extract start len inner.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.extract)
-        (toExpr inner.width)
-        startExpr
-        lenExpr
-        inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
-          startExpr
-          lenExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨len, bvExpr, proof, expr⟩
-    | BitVec.rotateLeft _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
-        innerExpr
-        .rotateLeft
-        ``BVUnOp.rotateLeft
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
-    | BitVec.rotateRight _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
-        innerExpr
-        .rotateRight
-        ``BVUnOp.rotateRight
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | _ => return none
-
-  /--
-  Reify `x` or abstract it as an atom.
-  Unless this function is called on something that is not a fixed-width `BitVec` it is always going
-  to return `some`.
-  -/
-  goOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-    let res ← go x
-    match res with
-    | some exp => return some exp
-    | none => bitVecAtom x
-
-  shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
-      (shiftOpName : Name) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
-    let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
-    let expr :=
-      mkApp3
-        (mkConst ``BVExpr.un)
-        (toExpr inner.width)
-        (mkApp (mkConst shiftOpName) (toExpr distance))
-        inner.expr
-    let congrProof :=
-      mkApp
-        (mkConst congrThm)
-        (toExpr distance)
-    let proof := unaryCongrProof inner innerExpr congrProof
-    return some ⟨inner.width, bvExpr, proof, expr⟩
-
-  rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
-      (rotateOpName : Name) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    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) :
-      M (Option ReifiedBVExpr) := do
-    let some distance ← getNatOrBvValue? β distanceExpr | return none
-    shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
-
-  shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
-      (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
-      (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let_expr BitVec _ ← β | return none
-    let some inner ← goOrAtom innerExpr | return none
-    let some distance ← goOrAtom distanceExpr | return none
-    let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr
-    let expr :=
-      mkApp4
-        (mkConst shiftOpName)
-        (toExpr inner.width)
-        (toExpr distance.width)
-        inner.expr
-        distance.expr
-    let congrProof :=
-      mkApp2
-        (mkConst congrThm)
-        (toExpr inner.width)
-        (toExpr distance.width)
-    let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof
-    return some ⟨inner.width, bvExpr, proof, expr⟩
-
-  binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
-    if h : rhs.width = lhs.width then
-      let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr)
-      let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
-      let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width)
-      let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm
-      return some ⟨lhs.width, bvExpr, proof, expr⟩
-    else
-      return none
-
-  binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (congrThm : Expr) :
-      M Expr := do
-    let lhsEval ← mkEvalExpr lhs.width lhs.expr
-    let lhsProof ← lhs.evalsAtAtoms
-    let rhsProof ← rhs.evalsAtAtoms
-    let rhsEval ← mkEvalExpr rhs.width rhs.expr
-    return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
-
-  unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
-      M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
-    let bvExpr := .un op inner.bvExpr
-    let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
-    let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
-    return some ⟨inner.width, bvExpr, proof, expr⟩
-
-  unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M Expr := do
-    let innerEval ← mkEvalExpr inner.width inner.expr
-    let innerProof ← inner.evalsAtAtoms
-    return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
-
-  goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← bitVecAtom x
-    let bvExpr : BVExpr width := .const bvVal
-    let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal)
-    let proof := do
-      let evalExpr ← mkEvalExpr width expr
-      return mkBVRefl width evalExpr
-    return some ⟨width, bvExpr, proof, expr⟩
+def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do
+  let bvExpr : BVExpr w := .const val
+  let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
+  let proof := do
+    let evalExpr ← ReifiedBVExpr.mkEvalExpr w expr
+    return ReifiedBVExpr.mkBVRefl w evalExpr
+  return ⟨w, bvExpr, proof, expr⟩
 
 end ReifiedBVExpr
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
index 39c014e3ac44..da62556ac44d 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
@@ -14,24 +14,7 @@ namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
 
 open Std.Tactic.BVDecide
-open Std.Tactic.BVDecide.Reflect.Bool
-
-/--
-A reified version of an `Expr` representing a `BVLogicalExpr`.
--/
-structure ReifiedBVLogical where
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVLogicalExpr
-  /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`
-  -/
-  expr : Expr
+open Lean.Meta
 
 namespace ReifiedBVLogical
 
@@ -47,11 +30,11 @@ def mkEvalExpr (expr : Expr) : M Expr := do
 /--
 Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
 -/
-def ofPred  (bvPred : ReifiedBVPred) : M (Option ReifiedBVLogical) := do
+def ofPred (bvPred : ReifiedBVPred) : M ReifiedBVLogical := do
   let boolExpr := .literal bvPred.bvPred
   let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
   let proof := bvPred.evalsAtAtoms
-  return some ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, proof, expr⟩
 
 /--
 Construct an uninterrpeted `Bool` atom from `t`.
@@ -61,81 +44,60 @@ def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do
   ofPred pred
 
 /--
-Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+Build a reified version of the constant `val`.
 -/
-partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
-  goOrAtom t
-where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVLogical) := do
-    match_expr t with
-    | Bool.true =>
-      let boolExpr := .const true
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true)
-      let proof := pure <| mkRefl (mkConst ``Bool.true)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.false =>
-      let boolExpr := .const false
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
-      let proof := pure <| mkRefl (mkConst ``Bool.false)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.not subExpr =>
-      let some sub ← goOrAtom subExpr | return none
-      let boolExpr := .not sub.bvExpr
-      let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
-      let proof := do
-        let subEvalExpr ← mkEvalExpr sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
-    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      match_expr α with
-      | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-      | BitVec _ => goPred t
-      | _ => return none
-    | _ => goPred t
-
-  /--
-  Reify `t` or abstract it as an atom.
-  Unless this function is called on something that is not a `Bool` it is always going to return `some`.
-  -/
-  goOrAtom (t : Expr) : M (Option ReifiedBVLogical) := do
-    match ← go t with
-    | some boolExpr => return some boolExpr
-    | none => boolAtom t
+def mkBoolConst (val : Bool) : M ReifiedBVLogical := do
+  let boolExpr := .const val
+  let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val)
+  let proof := pure <| ReifiedBVLogical.mkRefl (toExpr val)
+  return ⟨boolExpr, proof, expr⟩
 
-  gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (congrThm : Name) :
-      M (Option ReifiedBVLogical) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
-    let boolExpr := .gate  gate lhs.bvExpr rhs.bvExpr
-    let expr :=
-      mkApp4
-        (mkConst ``BoolExpr.gate)
-        (mkConst ``BVPred)
-        (toExpr gate)
-        lhs.expr
-        rhs.expr
-    let proof := do
-      let lhsEvalExpr ← mkEvalExpr lhs.expr
-      let rhsEvalExpr ← mkEvalExpr rhs.expr
-      let lhsProof ← lhs.evalsAtAtoms
-      let rhsProof ← rhs.evalsAtAtoms
-      return mkApp6
-        (mkConst congrThm)
-        lhsExpr rhsExpr
-        lhsEvalExpr rhsEvalExpr
-        lhsProof rhsProof
-    return some ⟨boolExpr, proof, expr⟩
+/--
+Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
+This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
+and `rhs`.
+-/
+def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : M ReifiedBVLogical := do
+  let congrThm := congrThmOfGate gate
+  let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
+  let expr :=
+    mkApp4
+      (mkConst ``BoolExpr.gate)
+      (mkConst ``BVPred)
+      (toExpr gate)
+      lhs.expr
+      rhs.expr
+  let proof := do
+    let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr
+    let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
+    return mkApp6
+      (mkConst congrThm)
+      lhsExpr rhsExpr
+      lhsEvalExpr rhsEvalExpr
+      lhsProof rhsProof
+  return ⟨boolExpr, proof, expr⟩
+where
+  congrThmOfGate (gate : Gate) : Name :=
+    match gate with
+    | .and => ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
+    | .xor => ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
+    | .beq => ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
+    | .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
 
-  goPred (t : Expr) : M (Option ReifiedBVLogical) := do
-    let some pred ← ReifiedBVPred.of t | return none
-    ofPred pred
+/--
+Construct the reified version of `Bool.not subExpr`.
+This function assumes that `subExpr` is the expression corresponding to `sub`.
+-/
+def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
+  let boolExpr := .not sub.bvExpr
+  let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
+  let proof := do
+    let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr
+    let subProof ← sub.evalsAtAtoms
+    return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
+  return ⟨boolExpr, proof, expr⟩
 
 end ReifiedBVLogical
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
index 108b2ebc15d8..76dae112c4b3 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
@@ -7,32 +7,14 @@ prelude
 import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVExpr
 
 /-!
-Provides the logic for reifying expressions consisting of predicates over `BitVec`s.
+Provides the logic for reifying predicates on `BitVec`.
 -/
 
 namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
 
-open Lean.Meta
 open Std.Tactic.BVDecide
-open Std.Tactic.BVDecide.Reflect.BitVec
-
-/--
-A reified version of an `Expr` representing a `BVPred`.
--/
-structure ReifiedBVPred where
-  /--
-  The reified expression.
-  -/
-  bvPred : BVPred
-  /--
-  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvPred`
-  -/
-  expr : Expr
+open Lean.Meta
 
 namespace ReifiedBVPred
 
@@ -63,70 +45,61 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
   return some ⟨bvExpr, proof, expr⟩
 
 /--
-Reify an `Expr` that is a predicate about `BitVec`.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+Construct the reified version of applying the predicate in `pred` to `lhs` and `rhs`.
+This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
+and `rhs`.
 -/
-partial def of (t : Expr) : M (Option ReifiedBVPred) := do
-  match ← go t with
-  | some pred => return some pred
-  | none => boolAtom t
+def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred) :
+    M (Option ReifiedBVPred) := do
+  if h : lhs.width = rhs.width then
+    let congrThm := congrThmofBinPred pred
+    let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
+    let expr :=
+      mkApp4
+        (mkConst ``BVPred.bin)
+        (toExpr lhs.width)
+        lhs.expr
+        (toExpr pred)
+        rhs.expr
+    let proof := do
+      let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+      let lhsProof ← lhs.evalsAtAtoms
+      let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
+      let rhsProof ← rhs.evalsAtAtoms
+      return mkApp7
+        (mkConst congrThm)
+        (toExpr lhs.width)
+        lhsExpr rhsExpr lhsEval rhsEval
+        lhsProof
+        rhsProof
+    return some ⟨bvExpr, proof, expr⟩
+  else
+    return none
 where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVPred) := do
-    match_expr t with
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      let_expr BitVec _ := α | return none
-      binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
-    | BitVec.ult _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
-    | BitVec.getLsbD _ subExpr idxExpr =>
-      let some sub ← ReifiedBVExpr.of subExpr | return none
-      let some idx ← getNatValue? idxExpr | return none
-      let bvExpr : BVPred := .getLsbD sub.bvExpr idx
-      let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
-      let proof := do
-        let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp5
-          (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
-          idxExpr
-          (toExpr sub.width)
-          subExpr
-          subEval
-          subProof
-      return some ⟨bvExpr, proof, expr⟩
-    | _ => return none
-
-  binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (congrThm : Name) :
-      M (Option ReifiedBVPred) := do
-    let some lhs ← ReifiedBVExpr.of lhsExpr | return none
-    let some rhs ← ReifiedBVExpr.of rhsExpr | return none
-    if h : lhs.width = rhs.width then
-      let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
-      let expr :=
-        mkApp4
-          (mkConst ``BVPred.bin)
-          (toExpr lhs.width)
-          lhs.expr
-          (toExpr pred)
-          rhs.expr
-      let proof := do
-        let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
-        let lhsProof ← lhs.evalsAtAtoms
-        let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
-        let rhsProof ← rhs.evalsAtAtoms
-        return mkApp7
-          (mkConst congrThm)
-          (toExpr lhs.width)
-          lhsExpr rhsExpr lhsEval rhsEval
-          lhsProof
-          rhsProof
-      return some ⟨bvExpr, proof, expr⟩
-    else
-      return none
+  congrThmofBinPred (pred : BVBinPred) : Name :=
+    match pred with
+    | .eq => ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
+    | .ult => ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
 
+/--
+Construct the reified version of `BitVec.getLsbD subExpr idx`.
+This function assumes that `subExpr` is the expression corresponding to `sub`.
+-/
+def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPred := do
+  let bvExpr : BVPred := .getLsbD sub.bvExpr idx
+  let idxExpr := toExpr idx
+  let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
+  let proof := do
+    let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
+    let subProof ← sub.evalsAtAtoms
+    return mkApp5
+      (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
+      idxExpr
+      (toExpr sub.width)
+      subExpr
+      subEval
+      subProof
+  return ⟨bvExpr, proof, expr⟩
 
 end ReifiedBVPred
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
new file mode 100644
index 000000000000..deb3fb3926e7
--- /dev/null
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical
+
+/-!
+Provides the logic for generating auxiliary lemmas during reification.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend
+
+open Std.Tactic.BVDecide
+open Lean.Meta
+
+/--
+This function adds the two lemmas:
+- `boolExpr = true → atomExpr = 1#1`
+- `boolExpr = false → atomExpr = 0#1`
+It assumes that `boolExpr` and `atomExpr` are the expressions corresponding to `bool` and `atom`.
+Furthermore it assumes that `atomExpr` is of the form `BitVec.ofBool boolExpr`.
+-/
+def addOfBoolLemmas (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
+    LemmaM Unit := do
+  let some ofBoolTrueLemma ← mkOfBoolTrueLemma bool atom boolExpr atomExpr | return ()
+  LemmaM.addLemma ofBoolTrueLemma
+  let some ofBoolFalseLemma ← mkOfBoolFalseLemma bool atom boolExpr atomExpr | return ()
+  LemmaM.addLemma ofBoolFalseLemma
+where
+  mkOfBoolTrueLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
+      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr true 1#1
+
+  mkOfBoolFalseLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
+      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr false 0#1
+
+  mkOfBoolLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr)
+     (boolVal : Bool) (resVal : BitVec 1) : M (Option SatAtBVLogical) := do
+    let lemmaName :=
+      match boolVal with
+      | .true => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_true
+      | .false => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_false
+
+    let boolValExpr := toExpr boolVal
+    let boolVal ← ReifiedBVLogical.mkBoolConst boolVal
+    let resExpr := toExpr resVal
+    let resValExpr ← ReifiedBVExpr.mkBVConst resVal
+
+    let eqBoolExpr ← mkAppM ``BEq.beq #[boolExpr, boolValExpr]
+    let eqBool ← ReifiedBVLogical.mkGate bool boolVal boolExpr boolValExpr .beq
+
+    let eqBVExpr ← mkAppM ``BEq.beq #[mkApp (mkConst ``BitVec.ofBool) boolExpr, resExpr]
+    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
+    let eqBV ← ReifiedBVLogical.ofPred eqBVPred
+
+    let trueExpr := mkConst ``Bool.true
+    let impExpr ← mkArrow (← mkEq eqBoolExpr trueExpr) (← mkEq eqBVExpr trueExpr)
+    let decideImpExpr ← mkAppOptM ``Decidable.decide #[some impExpr, none]
+    let imp ← ReifiedBVLogical.mkGate eqBool eqBV eqBoolExpr eqBVExpr .imp
+
+    let proof := do
+      let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
+      let congrProof ← imp.evalsAtAtoms
+      let lemmaProof := mkApp (mkConst lemmaName) boolExpr
+      return mkApp4
+        (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
+        decideImpExpr
+        evalExpr
+        congrProof
+        lemmaProof
+    return some ⟨imp.bvExpr, proof, imp.expr⟩
+
+end Frontend
+end Lean.Elab.Tactic.BVDecide
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
new file mode 100644
index 000000000000..dffe381999f3
--- /dev/null
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -0,0 +1,398 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedLemmas
+
+/-!
+Reifies `BitVec` problems with boolean substructure.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend
+
+open Std.Tactic.BVDecide
+open Lean.Meta
+
+mutual
+
+/--
+Reify an `Expr` that's a constant-width `BitVec`.
+Unless this function is called on something that is not a constant-width `BitVec` it is always
+going to return `some`.
+-/
+partial def ReifiedBVExpr.of (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
+  goOrAtom x
+where
+  /--
+  Reify `x`, returns `none` if the reification procedure failed.
+  -/
+  go (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    match_expr x with
+    | BitVec.ofNat _ _ => goBvLit x
+    | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
+    | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
+    | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
+    | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
+    | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
+    | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
+    | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
+    | BitVec.sdiv _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
+    | Complement.complement _ _ innerExpr =>
+      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
+        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
+        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
+        distance
+        innerExpr
+        .arithShiftRightConst
+        ``BVUnOp.arithShiftRightConst
+        ``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
+        let innerProof ← inner.evalsAtAtoms
+        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
+      let bvExpr := .signExtend newWidth inner.bvExpr
+      let expr :=
+        mkApp3
+          (mkConst ``BVExpr.signExtend)
+          (toExpr inner.width)
+          newWidthExpr
+          inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
+          newWidthExpr
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨newWidth, bvExpr, proof, expr⟩
+    | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
+      let some lhs ← goOrAtom lhsExpr | return none
+      let some rhs ← goOrAtom rhsExpr | return none
+      let bvExpr := .append lhs.bvExpr rhs.bvExpr
+      let expr := mkApp4 (mkConst ``BVExpr.append)
+        (toExpr lhs.width)
+        (toExpr rhs.width)
+        lhs.expr rhs.expr
+      let proof := do
+        let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+        let lhsProof ← lhs.evalsAtAtoms
+        let rhsProof ← rhs.evalsAtAtoms
+        let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
+        return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
+          (toExpr lhs.width) (toExpr rhs.width)
+          lhsExpr lhsEval
+          rhsExpr rhsEval
+          lhsProof rhsProof
+      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
+    | BitVec.replicate _ nExpr innerExpr =>
+      let some inner ← goOrAtom innerExpr | return none
+      let some n ← getNatValue? nExpr | return none
+      let bvExpr := .replicate n inner.bvExpr
+      let expr := mkApp3 (mkConst ``BVExpr.replicate)
+        (toExpr inner.width)
+        (toExpr n)
+        inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
+          (toExpr n)
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨inner.width * n, bvExpr, proof, expr⟩
+    | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
+      let some start ← getNatValue? startExpr | return none
+      let some len ← getNatValue? lenExpr | return none
+      let some inner ← goOrAtom innerExpr | return none
+      let bvExpr := .extract start len inner.bvExpr
+      let expr := mkApp4 (mkConst ``BVExpr.extract)
+        (toExpr inner.width)
+        startExpr
+        lenExpr
+        inner.expr
+      let proof := do
+        let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+        let innerProof ← inner.evalsAtAtoms
+        return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
+          startExpr
+          lenExpr
+          (toExpr inner.width)
+          innerExpr
+          innerEval
+          innerProof
+      return some ⟨len, bvExpr, proof, expr⟩
+    | BitVec.rotateLeft _ innerExpr distanceExpr =>
+      rotateReflection
+        distanceExpr
+        innerExpr
+        .rotateLeft
+        ``BVUnOp.rotateLeft
+        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
+    | BitVec.rotateRight _ innerExpr distanceExpr =>
+      rotateReflection
+        distanceExpr
+        innerExpr
+        .rotateRight
+        ``BVUnOp.rotateRight
+        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
+    | BitVec.ofBool boolExpr =>
+      let some bool ← ReifiedBVLogical.of boolExpr | return none
+      let atomExpr := (mkApp (mkConst ``BitVec.ofBool) boolExpr)
+      let some atom ← ReifiedBVExpr.bitVecAtom atomExpr | return none
+      addOfBoolLemmas bool atom boolExpr atomExpr
+      return some atom
+    | _ => return none
+
+  /--
+  Reify `x` or abstract it as an atom.
+  Unless this function is called on something that is not a fixed-width `BitVec` it is always going
+  to return `some`.
+  -/
+  goOrAtom (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    let res ← go x
+    match res with
+    | some exp => return some exp
+    | none => ReifiedBVExpr.bitVecAtom x
+
+  shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
+      (shiftOpName : Name) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some inner ← goOrAtom innerExpr | return none
+    let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
+    let expr :=
+      mkApp3
+        (mkConst ``BVExpr.un)
+        (toExpr inner.width)
+        (mkApp (mkConst shiftOpName) (toExpr distance))
+        inner.expr
+    let congrProof :=
+      mkApp
+        (mkConst congrThm)
+        (toExpr distance)
+    let proof := unaryCongrProof inner innerExpr congrProof
+    return some ⟨inner.width, bvExpr, proof, expr⟩
+
+  rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
+      (rotateOpName : Name) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    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 (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
+      (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
+      (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let_expr BitVec _ ← β | return none
+    let some inner ← goOrAtom innerExpr | return none
+    let some distance ← goOrAtom distanceExpr | return none
+    let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr
+    let expr :=
+      mkApp4
+        (mkConst shiftOpName)
+        (toExpr inner.width)
+        (toExpr distance.width)
+        inner.expr
+        distance.expr
+    let congrProof :=
+      mkApp2
+        (mkConst congrThm)
+        (toExpr inner.width)
+        (toExpr distance.width)
+    let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof
+    return some ⟨inner.width, bvExpr, proof, expr⟩
+
+  binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some lhs ← goOrAtom lhsExpr | return none
+    let some rhs ← goOrAtom rhsExpr | return none
+    if h : rhs.width = lhs.width then
+      let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr)
+      let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
+      let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width)
+      let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm
+      return some ⟨lhs.width, bvExpr, proof, expr⟩
+    else
+      return none
+
+  binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (congrThm : Expr) :
+      M Expr := do
+    let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
+    let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
+    return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
+
+  unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
+      LemmaM (Option ReifiedBVExpr) := do
+    let some inner ← goOrAtom innerExpr | return none
+    let bvExpr := .un op inner.bvExpr
+    let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
+    let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
+    return some ⟨inner.width, bvExpr, proof, expr⟩
+
+  unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M Expr := do
+    let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
+    let innerProof ← inner.evalsAtAtoms
+    return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
+
+  goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
+    let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x
+    ReifiedBVExpr.mkBVConst bvVal
+
+/--
+Reify an `Expr` that is a predicate about `BitVec`.
+Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+-/
+partial def ReifiedBVPred.of (t : Expr) : LemmaM (Option ReifiedBVPred) := do
+  match ← go t with
+  | some pred => return some pred
+  | none => ReifiedBVPred.boolAtom t
+where
+  /--
+  Reify `t`, returns `none` if the reification procedure failed.
+  -/
+  go (t : Expr) : LemmaM (Option ReifiedBVPred) := do
+    match_expr t with
+    | BEq.beq α _ lhsExpr rhsExpr =>
+      let_expr BitVec _ := α | return none
+      binaryReflection lhsExpr rhsExpr .eq
+    | BitVec.ult _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .ult
+    | BitVec.getLsbD _ subExpr idxExpr =>
+      let some sub ← ReifiedBVExpr.of subExpr | return none
+      let some idx ← getNatValue? idxExpr | return none
+      return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx)
+    | _ => return none
+
+  binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) : LemmaM (Option ReifiedBVPred) := do
+    let some lhs ← ReifiedBVExpr.of lhsExpr | return none
+    let some rhs ← ReifiedBVExpr.of rhsExpr | return none
+    ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred
+
+/--
+Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
+Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+-/
+partial def ReifiedBVLogical.of (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+  goOrAtom t
+where
+  /--
+  Reify `t`, returns `none` if the reification procedure failed.
+  -/
+  go (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    match_expr t with
+    | Bool.true => ReifiedBVLogical.mkBoolConst true
+    | Bool.false => ReifiedBVLogical.mkBoolConst false
+    | Bool.not subExpr =>
+      let some sub ← goOrAtom subExpr | return none
+      return some (← ReifiedBVLogical.mkNot sub subExpr)
+    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and
+    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor
+    | BEq.beq α _ lhsExpr rhsExpr =>
+      match_expr α with
+      | Bool => gateReflection lhsExpr rhsExpr .beq
+      | BitVec _ => goPred t
+      | _ => return none
+    | _ => goPred t
+
+  /--
+  Reify `t` or abstract it as an atom.
+  Unless this function is called on something that is not a `Bool` it is always going to return `some`.
+  -/
+  goOrAtom (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    match ← go t with
+    | some boolExpr => return some boolExpr
+    | none => ReifiedBVLogical.boolAtom t
+
+  gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) :
+      LemmaM (Option ReifiedBVLogical) := do
+    let some lhs ← goOrAtom lhsExpr | return none
+    let some rhs ← goOrAtom rhsExpr | return none
+    ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate
+
+  goPred (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    let some pred ← ReifiedBVPred.of t | return none
+    ReifiedBVLogical.ofPred pred
+
+end
+
+end Frontend
+end Lean.Elab.Tactic.BVDecide
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
index 9f653f5f6f73..64f0349fcef1 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reify
 
 /-!
 This module is the main entry point for reifying `BitVec` problems with boolean substructure.
@@ -19,29 +19,12 @@ namespace Frontend
 open Lean.Meta
 open Std.Tactic.BVDecide
 
-/--
-A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
--/
-structure SatAtBVLogical where
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVLogicalExpr
-  /--
-  A proof that `bvExpr.eval atomsAssignment = true`.
-  -/
-  satAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`
-  -/
-  expr : Expr
-
 namespace SatAtBVLogical
 
 /--
 Reify an `Expr` that is a proof of some boolean structure on top of predicates about `BitVec`s.
 -/
-partial def of (h : Expr) : M (Option SatAtBVLogical) := do
+partial def of (h : Expr) : LemmaM (Option SatAtBVLogical) := do
   let t ← instantiateMVars (← whnfR (← inferType h))
   match_expr t with
   | Eq α lhsExpr rhsExpr =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
index 8797391ebafd..e389699cb177 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
@@ -18,6 +18,7 @@ inductive Gate
   | and
   | xor
   | beq
+  | imp
 
 namespace Gate
 
@@ -25,11 +26,13 @@ def toString : Gate → String
   | and => "&&"
   | xor => "^^"
   | beq => "=="
+  | imp => "->"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
+  | imp => (· → ·)
 
 end Gate
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
index b2143d654408..d6443b8323a5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
@@ -59,6 +59,10 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
+      | .imp =>
+        let ret := aig.mkImpCached input
+        have := LawfulOperator.le_size (f := mkImpCached) aig input
+        ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
 
 variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]
 
@@ -96,6 +100,9 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
+    | imp =>
+      simp only [go]
+      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
 
 theorem ofBoolExprCached.go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 95c2a7ce3c44..35824b3d76ff 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -59,6 +59,8 @@ attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
 attribute [bv_normalize] BitVec.not_not
+attribute [bv_normalize] BitVec.ofBool_true
+attribute [bv_normalize] BitVec.ofBool_false
 
 end Constant
 
@@ -240,12 +242,6 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
 
-@[bv_normalize]
-theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
-    BitVec.ofBool (a.getLsbD i) = a.extractLsb' i 1 := by
-  ext j
-  simp
-
 @[bv_normalize]
 theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
     a[i] = a.getLsbD i := by
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index 93e729b537ed..09142cd69b1f 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -122,6 +122,16 @@ theorem sdiv_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (BitVec.sdiv lhs' rhs') = (BitVec.sdiv lhs rhs) := by
   simp[*]
 
+theorem ofBool_true (b : Bool) :
+    decide ((b == true) = true → (BitVec.ofBool b == 1#1) = true) = true := by
+  revert b
+  decide
+
+theorem ofBool_false (b : Bool) :
+    decide ((b == false) = true → (BitVec.ofBool b == 0#1) = true) = true := by
+  revert b
+  decide
+
 end BitVec
 
 namespace Bool
@@ -141,9 +151,16 @@ theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' == rhs') = (lhs == rhs) := by
   simp[*]
 
+theorem imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
+    (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
+  simp[*]
+
 theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by
   cases h₁; cases h₂
 
+theorem lemma_congr (x x' : Bool) (h1 : x' = x) (h2 : x = true) : x' = true := by
+  simp[*]
+
 end Bool
 
 open Std.Sat
diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean
index 26e5f517935f..a9fe997c165c 100644
--- a/tests/lean/run/bv_bitwise.lean
+++ b/tests/lean/run/bv_bitwise.lean
@@ -30,3 +30,11 @@ theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 63 = (x ^^^ ~~~x).
 
 theorem bitwise_unit_7 (x : BitVec 32) : x ^^^ 123#32 = 123#'(by decide) ^^^ x := by
   bv_decide
+
+theorem bitwise_unit_8 (x : BitVec 32) : BitVec.ofBool (x.getLsbD 0) = x.extractLsb' 0 1 := by
+  bv_decide
+
+theorem bitwise_unit_9 (x y : BitVec 32) :
+    BitVec.ofBool (x.getLsbD 0 ^^ y.getLsbD 0) = BitVec.ofBool ((x ^^^ y).getLsbD 0) := by
+  bv_decide
+
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 90982c1af2b6..c9cc36676968 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -62,8 +62,8 @@ example {x : BitVec 16} : x >>> 0 = x := by bv_normalize
 example {x : BitVec 16} : 0 < x ↔ (x != 0) := by bv_normalize
 example {x : BitVec 16} : ¬(-1#16 < x) := by bv_normalize
 example {x : BitVec 16} : BitVec.replicate 0 x = 0 := by bv_normalize
-example {x : BitVec 16} : BitVec.ofBool (x.getLsbD i) = x.extractLsb' i 1 := by bv_normalize
-example {x : BitVec 16} {i} {h} : BitVec.ofBool (x[i]'h) = x.extractLsb' i 1 := by bv_normalize
+example : BitVec.ofBool true = 1 := by bv_normalize
+example : BitVec.ofBool false = 0 := by bv_normalize
 example {x : BitVec 16} {i} {h} : x[i] = x.getLsbD i := by bv_normalize
 example {x y : BitVec 1} : x + y = x ^^^ y := by bv_normalize
 example {x y : BitVec 1} : x * y = x &&& y := by bv_normalize