diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean
index c5f4867229..6dbcba855f 100644
--- a/src/Std/Sat/AIG/Cached.lean
+++ b/src/Std/Sat/AIG/Cached.lean
@@ -49,8 +49,8 @@ A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is
 programming, for proving purposes use `AIG.mkGate` and equality theorems to this one.
 -/
 @[inline]
-def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
-  ⟨aig, ⟨0, val, aig.hzero⟩⟩
+def mkConstCached (aig : AIG α) (val : Bool) : Ref aig :=
+  ⟨0, val, aig.hzero⟩
 
 /--
 A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for
@@ -88,7 +88,9 @@ where
       let rhsVal := AIG.getConstant ⟨decls, cache, hdag, hzero, hconst⟩ input.rhs
       match lhsVal, rhsVal with
       -- Boundedness
-      | .some false, _ | _, .some false => mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
+      | .some false, _ | _, .some false =>
+        let ref := mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
+        ⟨⟨decls, cache, hdag, hzero, hconst⟩, ref⟩
       -- Left Neutrality
       | .some true, _ => ⟨⟨decls, cache, hdag, hzero, hconst⟩, ⟨rhs, rinv, by assumption⟩⟩
       -- Right Neutrality
@@ -97,9 +99,12 @@ where
       | _, _ =>
         if lhs == rhs then
            -- Idempotency
-          if linv == rinv then ⟨⟨decls, cache, hdag, hzero, hconst⟩, ⟨lhs, linv, by assumption⟩⟩
+          if linv == rinv then
+            ⟨⟨decls, cache, hdag, hzero, hconst⟩, ⟨lhs, linv, by assumption⟩⟩
           -- Contradiction
-          else mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
+          else
+            let ref := mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
+            ⟨⟨decls, cache, hdag, hzero, hconst⟩, ref⟩
         else
           -- Gate couldn't be simplified
           let g := decls.size
diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean
index 4f1b9afbd9..ddc61217ba 100644
--- a/src/Std/Sat/AIG/CachedGatesLemmas.lean
+++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean
@@ -61,7 +61,7 @@ instance : LawfulOperator α Ref mkNotCached where
 @[simp]
 theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} :
     ⟦aig.mkNotCached gate, assign⟧ = !⟦aig, gate, assign⟧ := by
-  simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]
+  simp [mkNotCached]
 
 theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) :
     aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size := by
@@ -103,7 +103,7 @@ instance : LawfulOperator α BinaryInput mkOrCached where
 theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} :
     ⟦aig.mkOrCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
   rw [← or_as_aig]
-  simp [mkOrCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
+  simp [mkOrCached]
 
 
 theorem mkXorCached_le_size (aig : AIG α) {input : BinaryInput aig} :
@@ -195,7 +195,7 @@ instance : LawfulOperator α BinaryInput mkImpCached where
 theorem denote_mkImpCached {aig : AIG α} {input : BinaryInput aig} :
     ⟦aig.mkImpCached input, assign⟧ = ( !⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
   rw [← imp_as_aig]
-  simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
+  simp [mkImpCached]
 
 end AIG
 
diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean
index af92a44e62..a01fbe71f2 100644
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -91,36 +91,12 @@ theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} :
     rw [denote_mkAtom_cached heq1]
   · simp [mkAtom, denote]
 
-theorem mkConstCached_aig (aig : AIG α) (val : Bool) : (aig.mkConstCached val).aig = aig := by
-  simp [mkConstCached]
-
-/--
-The AIG produced by `AIG.mkConstCached` agrees with the input AIG on all indices that are valid for
-both.
--/
-theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
-    (aig.mkConstCached val).aig.decls[idx]'h = aig.decls[idx] := by
-  simp [mkConstCached_aig]
-
-/--
-`AIG.mkConstCached` never shrinks the underlying AIG.
--/
-theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
-    aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size := by
-  simp [mkConstCached_aig]
-
-instance : LawfulOperator α (fun _ => Bool) mkConstCached where
-  le_size := mkConstCached_le_size
-  decl_eq := by
-    intros
-    apply mkConstCached_decl_eq
-
 /--
 The central equality theorem between `mkConstCached` and `mkConst`.
 -/
 @[simp]
-theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} :
-    ⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧ := by
+theorem denote_mkConstCached {aig : AIG α} :
+    ⟦aig, aig.mkConstCached val, assign⟧ = val := by
   simp only [mkConstCached, denote_mkConst]
   unfold denote denote.go
   split
@@ -150,18 +126,16 @@ theorem mkGateCached.go_le_size (aig : AIG α) (input : BinaryInput aig) :
   dsimp only [go]
   split
   · simp
-  · split <;> try simp [mkConstCached_le_size]
+  · split <;> try simp
     split
-    · split
-      · simp
-      · simp [mkConstCached_le_size]
+    · split <;> simp
     · simp
 
 /--
 `AIG.mkGateCached` never shrinks the underlying AIG.
 -/
-theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig)
-    : aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
+theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig) :
+    aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
   dsimp only [mkGateCached]
   split
   · apply mkGateCached.go_le_size
@@ -178,11 +152,9 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
       simp
     · split at hres
       · rw [← hres]
-        intros
-        rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
+        simp
       · rw [← hres]
-        intros
-        rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
+        simp
       · rw [← hres]
         intros
         simp
@@ -196,7 +168,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
             simp
           · rw [← hres]
             intros
-            rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
+            simp
         · rw [← hres]
           dsimp only
           intro idx h1 h2
diff --git a/src/Std/Sat/AIG/LawfulOperator.lean b/src/Std/Sat/AIG/LawfulOperator.lean
index 15abef39da..c814ed7482 100644
--- a/src/Std/Sat/AIG/LawfulOperator.lean
+++ b/src/Std/Sat/AIG/LawfulOperator.lean
@@ -30,6 +30,11 @@ structure IsPrefix (decls1 decls2 : Array (Decl α)) : Prop where
     -/
     idx_eq : ∀ idx (h : idx < decls1.size), decls2[idx]'(by omega) = decls1[idx]'h
 
+theorem IsPrefix.rfl {decls : Array (Decl α)} : IsPrefix decls decls := by
+  apply IsPrefix.of
+  · simp
+  · simp
+
 @[simp]
 theorem IsPrefix_push {decls : Array (Decl α)} : IsPrefix decls (decls.push decl) := by
   apply IsPrefix.of
diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean
index bee1c0e796..1affc224e5 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Fold.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean
@@ -19,14 +19,8 @@ variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α}
 def fold (aig : AIG α) (vec : RefVec aig len)
     (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] :
     Entrypoint α :=
-  let res := aig.mkConstCached true
-  let aig := res.aig
-  let acc := res.ref
-  let input := vec.cast <| by
-    intros
-    apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
-    omega
-  go aig acc 0 len input func
+  let acc := aig.mkConstCached true
+  go aig acc 0 len vec func
 where
   @[specialize]
   go (aig : AIG α) (acc : Ref aig) (idx : Nat) (len : Nat) (input : RefVec aig len)
@@ -63,8 +57,7 @@ theorem fold_le_size {aig : AIG α} (vec : RefVec aig len)
     aig.decls.size ≤ (fold aig vec func).1.decls.size := by
   unfold fold
   dsimp only
-  refine Nat.le_trans ?_ (by apply fold.go_le_size)
-  apply LawfulOperator.le_size (f := mkConstCached)
+  apply fold.go_le_size
 
 theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig len)
     (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] :
@@ -95,9 +88,6 @@ theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len)
   unfold fold
   dsimp only
   rw [fold.go_decl_eq]
-  rw [LawfulOperator.decl_eq (f := mkConstCached)]
-  apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
-  assumption
 
 theorem fold_lt_size_of_lt_aig_size (aig : AIG α) (vec : RefVec aig len)
     (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func]
@@ -177,18 +167,7 @@ theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) :
     (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧) := by
   unfold fold
   rw [fold.denote_go_and]
-  · simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst,
-    Nat.zero_le, get_cast, Ref.cast_eq, true_implies, true_and]
-    constructor
-    · intro h idx hidx
-      specialize h idx hidx
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] at h
-      rw [← h]
-    · intro h idx hidx
-      specialize h idx hidx
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)]
-      · simp only [← h]
-      · apply RefVec.hrefs
+  · simp
   · omega
 
 end RefVec
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
index 6fdc9af129..b08a211cc5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
@@ -21,64 +21,20 @@ namespace bitblast
 
 variable [Hashable α] [DecidableEq α]
 
-def blastConst (aig : AIG α) (val : BitVec w) : AIG.RefVecEntry α w :=
+def blastConst (aig : AIG α) (val : BitVec w) : AIG.RefVec aig w :=
   go aig val 0 (.emptyWithCapacity w) (by omega)
 where
   go (aig : AIG α) (val : BitVec w) (curr : Nat) (s : AIG.RefVec aig curr) (hcurr : curr ≤ w) :
-      AIG.RefVecEntry α w :=
+      AIG.RefVec aig w :=
     if hcurr : curr < w then
-      let res := aig.mkConstCached (val.getLsbD curr)
-      let aig := res.aig
-      let bitRef := res.ref
-      let s := s.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
+      let bitRef := aig.mkConstCached (val.getLsbD curr)
       let s := s.push bitRef
       go aig val (curr + 1) s (by omega)
     else
       have hcurr : curr = w := by omega
-      ⟨aig, hcurr ▸ s⟩
+      hcurr ▸ s
   termination_by w - curr
 
-theorem blastConst.go_le_size {aig : AIG α} (curr : Nat) (s : AIG.RefVec aig curr) (val : BitVec w)
-    (hcurr : curr ≤ w) :
-    aig.decls.size ≤ (go aig val curr s hcurr).aig.decls.size := by
-  unfold go
-  split
-  · dsimp only
-    refine Nat.le_trans ?_ (by apply go_le_size)
-    apply AIG.LawfulOperator.le_size
-  · simp
-termination_by w - curr
-
-theorem blastConst.go_decl_eq {aig : AIG α} (i : Nat) (s : AIG.RefVec aig i) (val : BitVec w)
-    (hi : i ≤ w) :
-    ∀ (curr : Nat) (h1) (h2),
-        (go aig val i s hi).aig.decls[curr]'h2 = aig.decls[curr]'h1 := by
-  generalize hgo : go aig val i s hi = res
-  unfold go at hgo
-  split at hgo
-  · dsimp only at hgo
-    rw [← hgo]
-    intro curr h1 h2
-    rw [blastConst.go_decl_eq]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-    apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-    assumption
-  · dsimp only at hgo
-    rw [← hgo]
-    intros
-    simp
-termination_by w - i
-
-instance : AIG.LawfulVecOperator α (fun _ w => BitVec w) blastConst where
-  le_size := by
-    intros
-    unfold blastConst
-    apply blastConst.go_le_size
-  decl_eq := by
-    intros
-    unfold blastConst
-    apply blastConst.go_decl_eq
-
 end bitblast
 end BVExpr
 
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 24eb087117..dcebe27271 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -129,9 +129,7 @@ where
       ⟨⟨res, this⟩, cache⟩
     | .const val =>
       let res := bitblast.blastConst aig val
-      have := AIG.LawfulVecOperator.le_size (f := bitblast.blastConst) ..
-      let cache := cache.cast this
-      ⟨⟨res, this⟩, cache⟩
+      ⟨⟨⟨aig, res⟩, by simp⟩, cache⟩
     | .bin lhsExpr op rhsExpr =>
       let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhsExpr cache
       let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhsExpr cache
@@ -316,7 +314,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
   unfold go
   split
   · rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)]
-  · rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
+  · simp
   · next op lhsExpr rhsExpr =>
     have hl := (goCache aig lhsExpr cache).result.property
     have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
index 34fd6bb4c0..c5558e52ab 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
@@ -168,10 +168,7 @@ def blastAdd (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry 
     blast aig ⟨rhs, lhs⟩
 where
   blast (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
-    let res := aig.mkConstCached false
-    let aig := res.aig
-    let cin := res.ref
-    let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
+    let cin := aig.mkConstCached false
     let ⟨lhs, rhs⟩ := input
     go aig lhs rhs 0 (by omega) cin (.emptyWithCapacity w)
 
@@ -238,16 +235,12 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
     intros
     unfold blast
     dsimp only
-    refine Nat.le_trans ?_ (by apply go_le_size)
-    apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
+    apply go_le_size
   decl_eq := by
     intros
     unfold blast
     dsimp only
     rw [go_decl_eq]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-    apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-    assumption
 
 end blastAdd
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
index 83d9ad7ec9..ef902795a0 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
@@ -28,19 +28,16 @@ structure ExtractTarget (aig : AIG α) (len : Nat) where
 def blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth) :
     AIG.RefVecEntry α newWidth :=
   let ⟨input, start⟩ := target
-  let res := aig.mkConstCached false
-  let aig := res.aig
-  let falseRef := res.ref
-  let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  ⟨aig, go input start falseRef 0 (by omega) (.emptyWithCapacity newWidth)⟩
+  ⟨aig, go input start 0 (by omega) (.emptyWithCapacity newWidth)⟩
 where
-  go {aig : AIG α} {w : Nat} (input : AIG.RefVec aig w) (start : Nat) (falseRef : AIG.Ref aig)
-      (curr : Nat) (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
+  go {aig : AIG α} {w : Nat} (input : AIG.RefVec aig w) (start : Nat) (curr : Nat)
+      (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
       AIG.RefVec aig newWidth :=
   if h : curr < newWidth then
+    let falseRef := aig.mkConstCached false
     let nextRef := input.getD (start + curr) falseRef
     let s := s.push nextRef
-    go input start falseRef (curr + 1) (by omega) s
+    go input start (curr + 1) (by omega) s
   else
     have : curr = newWidth := by omega
     this ▸ s
@@ -50,12 +47,11 @@ instance : AIG.LawfulVecOperator α ExtractTarget blastExtract where
   le_size := by
     intros
     unfold blastExtract
-    dsimp only
-    apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
+    simp
   decl_eq := by
     intros
     unfold blastExtract
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
+    simp
 
 end bitblast
 end BVExpr
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
index 6aa350278d..2936e8d4c7 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
@@ -24,25 +24,11 @@ structure GetLsbDTarget (aig : AIG α) where
   vec : AIG.RefVec aig w
   idx : Nat
 
-def blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) : AIG.Entrypoint α :=
+def blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) : AIG.Ref aig :=
   if h : target.idx < target.w then
-    ⟨aig, target.vec.get target.idx h⟩
+    target.vec.get target.idx h
   else
-    AIG.mkConstCached aig false
-
-instance : AIG.LawfulOperator α GetLsbDTarget blastGetLsbD where
-  le_size := by
-    intros
-    unfold blastGetLsbD
-    split
-    · simp
-    · apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
-  decl_eq := by
-    intros
-    unfold blastGetLsbD
-    split
-    · simp
-    · rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
+    aig.mkConstCached false
 
 end BVPred
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
index 0985568ca3..3190154cae 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
@@ -41,11 +41,7 @@ where
       ⟨aig, h ▸ .empty⟩
     else
       have : 0 < w := by omega
-      let res := blastConst aig 0
-      let aig := res.aig
-      let zero := res.vec
-      have := AIG.LawfulVecOperator.le_size (f := blastConst) ..
-      let input := input.cast this
+      let zero := blastConst aig 0
       let ⟨lhs, rhs⟩ := input
       let res := AIG.RefVec.ite aig ⟨rhs.get 0 (by assumption), lhs, zero⟩
       let aig := res.aig
@@ -139,8 +135,7 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
     · simp
     · dsimp only
       refine Nat.le_trans ?_ (by apply blastMul.go_le_size)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
-      apply AIG.LawfulVecOperator.le_size (f := blastConst)
+      apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
   decl_eq := by
     intros
     unfold blast
@@ -149,12 +144,8 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
     · dsimp only
       rw [blastMul.go_decl_eq]
       rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-        assumption
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
+      assumption
 
 end blastMul
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
index 4515ead9b3..ece1fad98d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
@@ -27,10 +27,7 @@ def blastNeg (aig : AIG α) (input : AIG.RefVec aig w) : AIG.RefVecEntry α w :=
   let aig := res.aig
   let notInput := res.vec
 
-  let res := blastConst aig 1#w
-  let aig := res.aig
-  let one := res.vec
-  let notInput := notInput.cast <| AIG.LawfulVecOperator.le_size (f := blastConst) ..
+  let one := blastConst aig 1#w
 
   blastAdd aig ⟨notInput, one⟩
 
@@ -40,20 +37,15 @@ instance : AIG.LawfulVecOperator α AIG.RefVec blastNeg where
     unfold blastNeg
     dsimp only
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastAdd)
-    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastConst)
     apply AIG.LawfulVecOperator.le_size (f := blastNot)
   decl_eq := by
     intros
     unfold blastNeg
     dsimp only
     rw [AIG.LawfulVecOperator.decl_eq (f := blastAdd)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastNot)]
     · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNot)
       assumption
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNot)
-      assumption
 
 end bitblast
 end BVExpr
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
index 93547c9684..3742ef478a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
@@ -35,12 +35,7 @@ where
       AIG.RefVecEntry α w :=
   if hidx : curr < w then
     if hdist : curr < distance then
-      let res := aig.mkConstCached false
-      let aig := res.aig
-      let zeroRef := res.ref
-      have hfinal := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-      let s := s.cast hfinal
-      let input := input.cast hfinal
+      let zeroRef := aig.mkConstCached false
       let s := s.push zeroRef
       go aig input distance (curr + 1) (by omega) s
     else
@@ -58,10 +53,8 @@ theorem blastShiftLeftConst.go_le_size (aig : AIG α) (distance : Nat) (input :
   split
   · dsimp only
     split
-    · refine Nat.le_trans ?_ (by apply go_le_size)
-      apply AIG.LawfulOperator.le_size
-    · refine Nat.le_trans ?_ (by apply go_le_size)
-      omega
+    · apply go_le_size
+    · apply go_le_size
   · simp
 termination_by w - curr
 
@@ -77,9 +70,6 @@ theorem blastShiftLeftConst.go_decl_eq (aig : AIG α) (distance : Nat) (input :
     · rw [← hgo]
       intro idx h1 h2
       rw [blastShiftLeftConst.go_decl_eq]
-      rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      assumption
     · rw [← hgo]
       intro idx h1 h2
       rw [blastShiftLeftConst.go_decl_eq]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
index 4a673c628a..26c7145d73 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
@@ -38,12 +38,7 @@ where
       let s := s.push (input.get (distance + curr) (by omega))
       go aig input distance (curr + 1) (by omega) s
     else
-      let res := aig.mkConstCached false
-      let aig := res.aig
-      let zeroRef := res.ref
-      have hfinal := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-      let s := s.cast hfinal
-      let input := input.cast hfinal
+      let zeroRef := aig.mkConstCached false
       let s := s.push zeroRef
       go aig input distance (curr + 1) (by omega) s
   else
@@ -58,10 +53,8 @@ theorem blastShiftRightConst.go_le_size (aig : AIG α) (distance : Nat) (input :
   split
   · dsimp only
     split
-    · refine Nat.le_trans ?_ (by apply go_le_size)
-      omega
-    · refine Nat.le_trans ?_ (by apply go_le_size)
-      apply AIG.LawfulOperator.le_size
+    · apply go_le_size
+    · apply go_le_size
   · simp
 termination_by w - curr
 
@@ -80,9 +73,6 @@ theorem blastShiftRightConst.go_decl_eq (aig : AIG α) (distance : Nat) (input :
     · rw [← hgo]
       intro idx h1 h2
       rw [blastShiftRightConst.go_decl_eq]
-      rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      assumption
   · simp [← hgo]
 termination_by w - curr
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
index eab57ee38f..37670280c1 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
@@ -57,28 +57,28 @@ structure BlastDivSubtractShiftOutput (old : AIG α) (w : Nat) where
   r : AIG.RefVec aig w
   hle : old.decls.size ≤ aig.decls.size
 
-def blastDivSubtractShift (aig : AIG α) (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
+def blastDivSubtractShift (aig : AIG α) (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) : BlastDivSubtractShiftOutput aig w :=
   let wn := wn - 1
   let wr := wr + 1
+  let falseRef := aig.mkConstCached false
   let res := blastUdiv.blastShiftConcat aig ⟨r, n.getD wn falseRef⟩
   let aig := res.aig
   let r' := res.vec
   have := AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat) ..
-  let falseRef := falseRef.cast this
-  let trueRef := trueRef.cast this
   let d := d.cast this
   let q := q.cast this
 
+  let falseRef := aig.mkConstCached false
   let res := blastUdiv.blastShiftConcat aig ⟨q, falseRef⟩
   let aig := res.aig
   let posQ := res.vec
   have := AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat) ..
-  let trueRef := trueRef.cast this
   let d := d.cast this
   let q := q.cast this
   let r' := r'.cast this
 
+  let trueRef := aig.mkConstCached true
   let res := blastUdiv.blastShiftConcat aig ⟨q, trueRef⟩
   let aig := res.aig
   let negQ := res.vec
@@ -130,9 +130,9 @@ def blastDivSubtractShift (aig : AIG α) (falseRef trueRef : AIG.Ref aig) (n d :
     apply AIG.LawfulVecOperator.le_size (f := blastShiftConcat)
   ⟨aig, wn, wr, nextQ, nextR, this⟩
 
-theorem blastDivSubtractShift_le_size (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
+theorem blastDivSubtractShift_le_size (aig : AIG α)
      (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
-    aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size := by
+    aig.decls.size ≤ (blastDivSubtractShift aig n d wn wr q r).aig.decls.size := by
   unfold blastDivSubtractShift
   dsimp only
   apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
@@ -143,11 +143,11 @@ theorem blastDivSubtractShift_le_size (aig : AIG α) (falseRef trueRef : AIG.Ref
   apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv.blastShiftConcat)
   apply AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat)
 
-theorem blastDivSubtractShift_decl_eq (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
-     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
+theorem blastDivSubtractShift_decl_eq (aig : AIG α) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (q r : AIG.RefVec aig w) :
     ∀ (idx : Nat) (h1) (h2),
-        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
-  generalize hres : blastDivSubtractShift aig falseRef trueRef n d wn wr q r = res
+        (blastDivSubtractShift aig n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hres : blastDivSubtractShift aig n d wn wr q r = res
   unfold blastDivSubtractShift at hres
   dsimp only at hres
   rw [← hres]
@@ -193,23 +193,21 @@ structure BlastUdivOutput (old : AIG α) (w : Nat) where
   r : AIG.RefVec aig w
   hle : old.decls.size ≤ aig.decls.size
 
-def go (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w)
+def go (aig : AIG α) (curr : Nat) (n d : AIG.RefVec aig w)
     (wn wr : Nat) (q r : AIG.RefVec aig w) : BlastUdivOutput aig w :=
   match curr with
   | 0 => ⟨aig, q, r, by omega⟩
   | curr + 1 =>
-    let res := blastDivSubtractShift aig falseRef trueRef n d wn wr q r
+    let res := blastDivSubtractShift aig n d wn wr q r
     let aig := res.aig
     let wn := res.wn
     let wr := res.wr
     let q := res.q
     let r := res.r
     have := res.hle
-    let falseRef := falseRef.cast this
-    let trueRef := trueRef.cast this
     let n := n.cast this
     let d := d.cast this
-    let res := go aig curr falseRef trueRef n d wn wr q r
+    let res := go aig curr n d wn wr q r
     let aig := res.aig
     let q := res.q
     let r := res.r
@@ -224,9 +222,9 @@ def go (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig) (n d : AIG.R
       apply AIG.LawfulVecOperator.le_size (f := blastShiftConcat)
     ⟨aig, q, r, this⟩
 
-theorem go_le_size (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
-    (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
-    aig.decls.size ≤ (go aig curr falseRef trueRef n d wn wr q r).aig.decls.size := by
+theorem go_le_size (aig : AIG α) (curr : Nat) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (q r : AIG.RefVec aig w) :
+    aig.decls.size ≤ (go aig curr n d wn wr q r).aig.decls.size := by
   unfold go
   dsimp only
   split
@@ -234,11 +232,11 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
   · refine Nat.le_trans ?_ (by apply go_le_size)
     apply blastUdiv.blastDivSubtractShift_le_size
 
-theorem go_decl_eq (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
-     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
+theorem go_decl_eq (aig : AIG α) (curr : Nat) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (q r : AIG.RefVec aig w) :
     ∀ (idx : Nat) (h1) (h2),
-        (go aig curr falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
-  generalize hgo : go aig curr falseRef trueRef n d wn wr q r = res
+        (go aig curr n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hgo : go aig curr n d wn wr q r = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo
@@ -254,39 +252,18 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
 end blastUdiv
 
 def blastUdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
-  let res := blastConst aig 0#w
-  let aig := res.aig
-  let zero := res.vec
-  let input := input.cast <| AIG.LawfulVecOperator.le_size (f := blastConst) ..
-
-  let res := aig.mkConstCached false
-  let aig := res.aig
-  let falseRef := res.ref
-  have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  let zero := zero.cast this
-  let input := input.cast this
-
-  let res := aig.mkConstCached true
-  let aig := res.aig
-  let trueRef := res.ref
-  have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  let falseRef := falseRef.cast this
-  let zero := zero.cast this
-  let input := input.cast this
-
+  let zero := blastConst aig 0#w
   let ⟨lhs, rhs⟩ := input
 
   let res := BVPred.mkEq aig ⟨rhs, zero⟩
   let aig := res.aig
   let discr := res.ref
   have := AIG.LawfulOperator.le_size (f := BVPred.mkEq) ..
-  let falseRef := falseRef.cast this
-  let trueRef := trueRef.cast this
   let zero := zero.cast this
   let lhs := lhs.cast this
   let rhs := rhs.cast this
 
-  let res := blastUdiv.go aig w falseRef trueRef lhs rhs w 0 zero zero
+  let res := blastUdiv.go aig w lhs rhs w 0 zero zero
   let aig := res.aig
   let divRes := res.q
   have := blastUdiv.go_le_size ..
@@ -301,38 +278,17 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUdiv where
     unfold blastUdiv
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
     refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkEq)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
-    apply AIG.LawfulVecOperator.le_size (f := blastConst)
+    apply AIG.LawfulOperator.le_size (f := BVPred.mkEq)
   decl_eq := by
     intros
     unfold blastUdiv
     rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
     rw [blastUdiv.go_decl_eq]
     rw [AIG.LawfulOperator.decl_eq (f := BVPred.mkEq)]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      assumption
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      assumption
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      assumption
     · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
       assumption
     · refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
       assumption
 
 end bitblast
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
index d873aee1ba..e445b2478a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
@@ -25,13 +25,10 @@ def mkUlt (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α :=
   let res := BVExpr.bitblast.blastNot aig rhsRefs
   let aig := res.aig
   let rhsNotRefs := res.vec
-  let res := aig.mkConstCached true
+  let trueRef := aig.mkConstCached true
   let aig := res.aig
-  let trueRef := res.ref
   let lhsRefs := lhsRefs.cast <| by
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
     apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast.blastNot)
-  let rhsNotRefs := rhsNotRefs.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
   let res := BVExpr.bitblast.mkOverflowBit aig ⟨_, ⟨lhsRefs, rhsNotRefs⟩, trueRef⟩
   let aig := res.aig
   let overflowRef := res.ref
@@ -44,7 +41,6 @@ instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkUlt where
     dsimp only
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkNotCached)
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVExpr.bitblast.mkOverflowBit)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
     apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast.blastNot)
   decl_eq := by
     intros
@@ -52,15 +48,10 @@ instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkUlt where
     dsimp only
     rw [AIG.LawfulOperator.decl_eq (f := AIG.mkNotCached)]
     rw [AIG.LawfulOperator.decl_eq (f := BVExpr.bitblast.mkOverflowBit)]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
     rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast.blastNot)]
     · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.blastNot)
       assumption
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.blastNot)
-      assumption
     · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.mkOverflowBit)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
       apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.blastNot)
       assumption
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
index c23a135273..7f0ddad837 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
@@ -22,39 +22,18 @@ namespace bitblast
 variable [Hashable α] [DecidableEq α]
 
 def blastUmod (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
-  let res := blastConst aig 0#w
-  let aig := res.aig
-  let zero := res.vec
-  let input := input.cast <| AIG.LawfulVecOperator.le_size (f := blastConst) ..
-
-  let res := aig.mkConstCached false
-  let aig := res.aig
-  let falseRef := res.ref
-  have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  let zero := zero.cast this
-  let input := input.cast this
-
-  let res := aig.mkConstCached true
-  let aig := res.aig
-  let trueRef := res.ref
-  have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  let falseRef := falseRef.cast this
-  let zero := zero.cast this
-  let input := input.cast this
-
+  let zero := blastConst aig 0#w
   let ⟨lhs, rhs⟩ := input
 
   let res := BVPred.mkEq aig ⟨rhs, zero⟩
   let aig := res.aig
   let discr := res.ref
   have := AIG.LawfulOperator.le_size (f := BVPred.mkEq) ..
-  let falseRef := falseRef.cast this
-  let trueRef := trueRef.cast this
   let zero := zero.cast this
   let lhs := lhs.cast this
   let rhs := rhs.cast this
 
-  let res := blastUdiv.go aig w falseRef trueRef lhs rhs w 0 zero zero
+  let res := blastUdiv.go aig w lhs rhs w 0 zero zero
   let aig := res.aig
   let modRes := res.r
   have := blastUdiv.go_le_size ..
@@ -69,38 +48,17 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUmod where
     unfold blastUmod
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
     refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkEq)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
-    apply AIG.LawfulVecOperator.le_size (f := blastConst)
+    apply AIG.LawfulOperator.le_size (f := BVPred.mkEq)
   decl_eq := by
     intros
     unfold blastUmod
     rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
     rw [blastUdiv.go_decl_eq]
     rw [AIG.LawfulOperator.decl_eq (f := BVPred.mkEq)]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      assumption
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      assumption
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
-      assumption
     · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
       assumption
     · refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
       assumption
 
 end bitblast
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
index edcb56f7fe..161a9f9473 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
@@ -34,12 +34,7 @@ where
         let s := s.push (input.get curr hcurr2)
         go aig w input newWidth (curr + 1) (by omega) s
       else
-        let res := aig.mkConstCached false
-        let aig := res.aig
-        let zeroRef := res.ref
-        have hcast := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-        let input := input.cast hcast
-        let s := s.cast hcast
+        let zeroRef := aig.mkConstCached false
         let s := s.push zeroRef
         go aig w input newWidth (curr + 1) (by omega) s
     else
@@ -56,10 +51,8 @@ theorem go_le_size (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
   split
   · dsimp only
     split
-    · refine Nat.le_trans ?_ (by apply go_le_size)
-      omega
-    · refine Nat.le_trans ?_ (by apply go_le_size)
-      apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
+    · apply go_le_size
+    · apply go_le_size
   · simp
 termination_by newWidth - curr
 
@@ -78,9 +71,6 @@ theorem go_decl_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
     · rw [← hgo]
       intro idx h1 h2
       rw [go_decl_eq]
-      rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
-      assumption
   · simp [← hgo]
 termination_by newWidth - curr
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
index 1647738281..43e2f90345 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
@@ -57,11 +57,7 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai
     -/
     let ⟨⟨⟨aig, refs⟩, hrefs⟩, cache⟩ := BVExpr.bitblast aig ⟨expr, cache⟩
     let res := blastGetLsbD aig ⟨refs, idx⟩
-    let cache := cache.cast (AIG.LawfulOperator.le_size (f := blastGetLsbD) ..)
-    have := by
-      apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsbD)
-      exact hrefs
-    ⟨⟨res, this⟩, cache⟩
+    ⟨⟨⟨aig, res⟩, hrefs⟩, cache⟩
 
 theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
     ∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
@@ -93,10 +89,7 @@ theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig)
         assumption
   | getLsbD expr idx =>
     simp only [bitblast]
-    rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)]
     rw [BVExpr.bitblast_decl_eq]
-    apply BVExpr.bitblast_lt_size_of_lt_aig_size
-    assumption
 
 theorem bitblast_le_size (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
     aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean
index 42c071d0d1..bcf0a0332f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean
@@ -28,8 +28,7 @@ where
     match expr with
     | .literal var => BVPred.bitblast aig ⟨var, cache⟩
     | .const val =>
-      have := LawfulOperator.le_size (f := mkConstCached) ..
-      ⟨⟨aig.mkConstCached val, this⟩, cache.cast this⟩
+      ⟨⟨⟨aig, aig.mkConstCached val⟩, by simp⟩, cache⟩
     | .not expr =>
       let ⟨⟨⟨aig, exprRef⟩, hexpr⟩, cache⟩ := go aig expr cache
       let ret := aig.mkNotCached exprRef
@@ -120,9 +119,7 @@ theorem go_lt_size_of_lt_aig_size (aig : AIG BVBit) (expr : BVLogicalExpr)
 theorem go_decl_eq (idx) (aig : AIG BVBit) (cache : BVExpr.Cache aig) (h : idx < aig.decls.size) (hbounds) :
     (go aig expr cache).result.val.aig.decls[idx]'hbounds = aig.decls[idx] := by
   induction expr generalizing aig with
-  | const =>
-    simp only [go]
-    rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
+  | const => simp [go]
   | literal =>
     simp only [go]
     rw [BVPred.bitblast_decl_eq]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
index 7e3491b8cb..06884a3dcc 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
@@ -31,8 +31,8 @@ theorem go_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.
   | const =>
     simp only [go]
     apply BVExpr.Cache.Inv_cast
-    apply LawfulOperator.isPrefix_aig (f := mkConstCached)
-    exact hinv
+    · apply IsPrefix.rfl
+    · exact hinv
   | literal =>
     simp only [go]
     apply BVPred.bitblast_Inv_of_Inv
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
index 4ffd685bdf..d2a0cb8a17 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
@@ -29,7 +29,7 @@ theorem go_get_aux (aig : AIG α) (c : BitVec w) (curr : Nat) (hcurr : curr ≤
     -- `generalize` would produce a type incorrect term as the proof term would talk about
     -- a `go` application instead of the fresh variable.
     ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
-        (go aig c curr s hcurr).vec.get idx (by omega) = (s.get idx hidx).cast hfoo := by
+        (go aig c curr s hcurr).get idx (by omega) = (s.get idx hidx).cast hfoo := by
   intro idx hidx
   generalize hgo : go aig c curr s hcurr = res
   unfold go at hgo
@@ -39,11 +39,6 @@ theorem go_get_aux (aig : AIG α) (c : BitVec w) (curr : Nat) (hcurr : curr ≤
     intro hfoo
     rw [go_get_aux]
     rw [AIG.RefVec.get_push_ref_lt]
-    · simp only [Ref.cast, Ref.mk.injEq]
-      rw [AIG.RefVec.get_cast]
-      · simp
-      · assumption
-    · apply go_le_size
   · dsimp only at hgo
     rw [← hgo]
     simp only [Nat.le_refl, get, Ref.gate_cast, Ref.mk.injEq, true_implies]
@@ -54,38 +49,17 @@ termination_by w - curr
 theorem go_get (aig : AIG α) (c : BitVec w)
     (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
     ∀ (idx : Nat) (hidx : idx < curr),
-        (go aig c curr s hcurr).vec.get idx (by omega)
-          =
-        (s.get idx hidx).cast (by apply go_le_size) := by
+        (go aig c curr s hcurr).get idx (by omega) = s.get idx hidx := by
   intros
   apply go_get_aux
-
-theorem go_denote_mem_prefix (aig : AIG α) (idx : Nat) (hidx)
-    (s : AIG.RefVec aig idx) (c : BitVec w) (start : Nat) (hstart) :
-    ⟦
-      (go aig c idx s hidx).aig,
-      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
-      assign
-    ⟧
-      =
-    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
-  apply IsPrefix.of
-  · intros
-    apply go_decl_eq
-  · intros
-    apply go_le_size
+  simp
 
 theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
     (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
     ∀ (idx : Nat) (hidx1 : idx < w),
         curr ≤ idx
           →
-        ⟦
-          (go aig c curr s hcurr).aig,
-          (go aig c curr s hcurr).vec.get idx hidx1,
-          assign
-        ⟧
+        ⟦aig, (go aig c curr s hcurr).get idx hidx1, assign⟧
           =
         c.getLsbD idx := by
   intro idx hidx1 hidx2
@@ -99,9 +73,7 @@ theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
       rw [go_get]
       rw [AIG.RefVec.get_push_ref_eq']
       · rw [← heq]
-        rw [go_denote_mem_prefix]
-        · simp
-        · simp [Ref.hgate]
+        simp
       · rw [heq]
     | inr =>
       rw [← hgo]
@@ -115,9 +87,7 @@ end blastConst
 @[simp]
 theorem denote_blastConst (aig : AIG α) (c : BitVec w) (assign : α → Bool) :
     ∀ (idx : Nat) (hidx : idx < w),
-        ⟦(blastConst aig c).aig, (blastConst aig c).vec.get idx hidx, assign⟧
-          =
-        c.getLsbD idx := by
+        ⟦aig, (blastConst aig c).get idx hidx, assign⟧ = c.getLsbD idx := by
   intros
   apply blastConst.go_denote_eq
   omega
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 a5d05af99b..4fea7b951d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -195,7 +195,7 @@ theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) :
     · exact hinv
   · rw [← hres]
     apply Cache.Inv_cast
-    · apply LawfulVecOperator.isPrefix_aig (f := blastConst)
+    · apply IsPrefix.rfl
     · exact hinv
   · next op lhsExpr rhsExpr =>
     dsimp only at hres
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
index ac411294a6..f75e70d0ac 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
@@ -216,19 +216,10 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
     unfold blast
     dsimp only
     rw [blastAdd.go_denote_eq _ 0 (by omega) _ _ _ _ assign lhs rhs _ _]
-    · simp only [BinaryRefVec.lhs_get_cast, Ref.cast_eq, BinaryRefVec.rhs_get_cast]
-      rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
-      rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
+    · simp
     · simp
     · omega
-    · intros
-      simp only [BinaryRefVec.lhs_get_cast, Ref.cast_eq]
-      rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
-      rw [hleft]
-    · intros
-      simp only [BinaryRefVec.rhs_get_cast, Ref.cast_eq]
-      rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
-      rw [hright]
+    · simp [hright]
   · assumption
 
 end blastAdd
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
index e650eedc4e..2f144e7876 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
@@ -24,11 +24,11 @@ variable [Hashable α] [DecidableEq α]
 namespace blastExtract
 
 theorem go_get_aux (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
-    (hcurr : curr ≤ newWidth) (falseRef : Ref aig) (s : RefVec aig curr) :
+    (hcurr : curr ≤ newWidth) (s : RefVec aig curr) :
     ∀ (idx : Nat) (hidx1 : idx < curr),
-        (go input lo falseRef curr hcurr s).get idx (by omega) = s.get idx hidx1 := by
+        (go input lo curr hcurr s).get idx (by omega) = s.get idx hidx1 := by
   intro idx hidx
-  generalize hgo : go input lo falseRef curr hcurr s = res
+  generalize hgo : go input lo curr hcurr s = res
   unfold go at hgo
   split at hgo
   · dsimp only at hgo
@@ -44,12 +44,14 @@ theorem go_get_aux (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
 termination_by newWidth - curr
 
 theorem go_get (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
-    (hcurr : curr ≤ newWidth) (falseRef : Ref aig) (s : RefVec aig curr) :
+    (hcurr : curr ≤ newWidth) (s : RefVec aig curr) :
     ∀ (idx : Nat) (hidx1 : idx < newWidth),
-        curr ≤ idx → (go input lo falseRef curr hcurr s).get idx hidx1 = input.getD (lo + idx) falseRef
+        curr ≤ idx → (go input lo curr hcurr s).get idx hidx1
+          =
+        input.getD (lo + idx) (aig.mkConstCached false)
     := by
   intro idx hidx1 hidx2
-  generalize hgo : go input lo falseRef curr hcurr s = res
+  generalize hgo : go input lo curr hcurr s = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo
@@ -90,8 +92,6 @@ theorem denote_blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth)
     · dsimp only
       split
       · rw [RefVec.get_in_bound]
-        rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
-        congr 1
       · rw [RefVec.get_out_bound]
         · simp
         · omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
index fbd100faae..3ecc05ea9a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
@@ -36,7 +36,7 @@ theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec
 
 @[simp]
 theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) (assign : α → Bool) :
-    ⟦blastGetLsbD aig target, assign⟧
+    ⟦aig, blastGetLsbD aig target, assign⟧
       =
     if h : target.idx < target.w then
       ⟦aig, target.vec.get target.idx h, assign⟧
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
index d07e3967b7..a8ec4c9731 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
@@ -144,12 +144,10 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
     · omega
     · intro idx hidx
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
       · simp [hleft]
       · simp [Ref.hgate]
     · intro idx hidx
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
       · simp [hright]
       · simp [Ref.hgate]
     · intro idx hidx
@@ -161,18 +159,12 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
       split
       · next heq =>
         rw [← hright] at heq
-        · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-          · simp [heq, hleft]
-          · simp [Ref.hgate]
-          · simp [Ref.hgate]
+        · simp [heq, hleft]
         · omega
       · next heq =>
         simp only [Bool.not_eq_true] at heq
         rw [← hright] at heq
-        · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-          · simp [heq]
-          · simp [Ref.hgate]
+        · simp [heq]
         · omega
 
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
index fc445e2d5c..7dabb7248d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
@@ -38,10 +38,7 @@ theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w
   dsimp only
   rw [denote_blastAdd]
   · intro idx hidx
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-    · simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
-      rw [denote_blastNot, htarget, BitVec.getLsbD_eq_getElem]
-    · simp [Ref.hgate]
+    simp [hidx, htarget]
   · simp
 
 end bitblast
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
index ef31e8289a..a6e5c7289f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
@@ -40,11 +40,6 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
       intros
       rw [go_get_aux]
       rw [AIG.RefVec.get_push_ref_lt]
-      · simp only [Ref.cast, Ref.mk.injEq]
-        rw [AIG.RefVec.get_cast]
-        · simp
-        · assumption
-      · apply go_le_size
     · rw [← hgo]
       intros
       rw [go_get_aux]
@@ -110,7 +105,8 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
           rw [go_get]
           rw [AIG.RefVec.get_push_ref_eq']
           · rw [go_denote_mem_prefix]
-            · simp
+            · simp only [Ref.cast_eq]
+              rw [denote_mkConstCached]
             · simp [Ref.hgate]
           · rw [heq]
         · omega
@@ -134,8 +130,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
         · next hidx =>
           rw [← hgo]
           rw [go_denote_eq]
-          · simp only [hidx, ↓reduceDIte, RefVec.get_cast, Ref.cast_eq]
-            rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
+          · simp [hidx]
           · omega
       · split
         · omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
index 72f8947d77..c70b328602 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
@@ -44,11 +44,6 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
       intros
       rw [go_get_aux]
       rw [AIG.RefVec.get_push_ref_lt]
-      · simp only [Ref.cast, Ref.mk.injEq]
-        rw [AIG.RefVec.get_cast]
-        · simp
-        · assumption
-      · apply go_le_size
   · dsimp only at hgo
     rw [← hgo]
     simp only [Nat.le_refl, get, Ref.gate_cast, Ref.mk.injEq, true_implies]
@@ -120,7 +115,8 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
           rw [go_get]
           rw [AIG.RefVec.get_push_ref_eq']
           · rw [go_denote_mem_prefix]
-            · simp
+            · simp only [Ref.cast_eq]
+              rw [denote_mkConstCached]
             · simp [Ref.hgate]
           · rw [heq]
     | inr =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
index 983792eff1..03f5672ee8 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
@@ -57,10 +57,10 @@ theorem denote_blastShiftConcat_eq_shiftConcat (aig : AIG α) (target : ShiftCon
   simp [BitVec.getLsbD_shiftConcat, hidx, denote_blastShiftConcat, hx, hb, ← BitVec.getLsbD_eq_getElem]
 
 
-theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
+theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α)
     (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
     ⟦
-      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
+      (blastDivSubtractShift aig n d wn wr q r).aig,
       ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩,
       assign
     ⟧
@@ -74,19 +74,16 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef
     apply blastDivSubtractShift_le_size
 
 theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
     (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
-    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
-    (hfalse : ⟦aig, falseRef, assign⟧ = false)
-    (htrue : ⟦aig, trueRef, assign⟧ = true)
-      :
+    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦
-        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
-        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx,
+        (blastDivSubtractShift aig n d wn wr q r).aig,
+        (blastDivSubtractShift aig n d wn wr q r).q.get idx hidx,
         assign
       ⟧
         =
@@ -113,7 +110,7 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
         · simp [hr]
         · rw [BVPred.denote_getD_eq_getLsbD]
           · simp [hleft]
-          · simp [hfalse]
+          · simp
       · intro idx hidx
         simp only [RefVec.get_cast, Ref.cast_eq]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
@@ -132,9 +129,7 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         · simp [hq]
         · simp [Ref.hgate]
-      · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-        · simp [hfalse]
-        · simp [Ref.hgate]
+      · rw [denote_mkConstCached]
     · intro h
       simp only [RefVec.get_cast, Ref.cast_eq]
       rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
@@ -145,24 +140,20 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         · simp [hq]
         · simp [Ref.hgate]
-      · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-        · simp [htrue]
-        · simp [Ref.hgate]
+      · rw [denote_mkConstCached]
   . simp [Ref.hgate]
 
 theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
     (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
-    (hfalse : ⟦aig, falseRef, assign⟧ = false)
       :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦
-        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
-        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r.get idx hidx,
+        (blastDivSubtractShift aig n d wn wr q r).aig,
+        (blastDivSubtractShift aig n d wn wr q r).r.get idx hidx,
         assign
       ⟧
         =
@@ -185,7 +176,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
         simp [hr]
       · rw [BVPred.denote_getD_eq_getLsbD]
         · exact hleft
-        · exact hfalse
+        · simp
     · next hdiscr =>
       rw [← Normalize.BitVec.lt_ult] at hdiscr
       simp only [Ref.cast_eq, id_eq, Int.reduceNeg, hdiscr, ↓reduceIte]
@@ -200,7 +191,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
         · simp [hr]
         · rw [BVPred.denote_getD_eq_getLsbD]
           · exact hleft
-          · exact hfalse
+          · simp
       · intro idx hidx
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
@@ -217,7 +208,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
       . dsimp only
         rw [BVPred.denote_getD_eq_getLsbD]
         · exact hleft
-        · exact hfalse
+        · simp
     . simp [Ref.hgate]
   · intro idx hidx
     rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
@@ -229,10 +220,10 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
 
 @[simp]
 theorem denote_blastDivSubtractShift_wn (aig : AIG α) (lhs rhs : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
       :
-    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
+    (blastDivSubtractShift aig n d wn wr q r).wn
       =
     (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wn := by
   unfold blastDivSubtractShift BitVec.divSubtractShift
@@ -241,10 +232,10 @@ theorem denote_blastDivSubtractShift_wn (aig : AIG α) (lhs rhs : BitVec w)
 
 @[simp]
 theorem denote_blastDivSubtractShift_wr (aig : AIG α) (lhs rhs : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
+    (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
       :
-    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
+    (blastDivSubtractShift aig n d wn wr q r).wr
       =
     (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wr := by
   unfold blastDivSubtractShift BitVec.divSubtractShift
@@ -252,18 +243,16 @@ theorem denote_blastDivSubtractShift_wr (aig : AIG α) (lhs rhs : BitVec w)
   split <;> simp
 
 theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
+    (n d q r : AIG.RefVec aig w) (wn wr : Nat)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
     (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
     (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
-    (hfalse : ⟦aig, falseRef, assign⟧ = false)
-    (htrue : ⟦aig, trueRef, assign⟧ = true)
       :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦
-        (go aig curr falseRef trueRef n d wn wr q r).aig,
-        (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx,
+        (go aig curr n d wn wr q r).aig,
+        (go aig curr n d wn wr q r).q.get idx hidx,
         assign
       ⟧
         =
@@ -295,8 +284,6 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hright
         · exact hq
         · exact hr
-        · exact hfalse
-        · exact htrue
       · intro idx hidx
         rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
         · rw [BitVec.divSubtractShift]
@@ -304,13 +291,6 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hleft
         · exact hright
         · exact hr
-        · exact hfalse
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [hfalse]
-        · simp [Ref.hgate]
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [htrue]
-        · simp [Ref.hgate]
     · next hdiscr =>
       rw [ih]
       · rfl
@@ -330,8 +310,6 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hright
         · exact hq
         · exact hr
-        · exact hfalse
-        · exact htrue
       · intro idx hidx
         rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
         · rw [BitVec.divSubtractShift]
@@ -339,28 +317,19 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hleft
         · exact hright
         · exact hr
-        · exact hfalse
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [hfalse]
-        · simp [Ref.hgate]
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [htrue]
-        · simp [Ref.hgate]
 
 theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w)
+    (n d q r : AIG.RefVec aig w)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
     (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = false)
     (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = false)
-    (hfalse : ⟦aig, falseRef, assign⟧ = false)
-    (htrue : ⟦aig, trueRef, assign⟧ = true)
     (hzero : 0#w < rhs)
       :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦
-        (go aig w falseRef trueRef n d w 0 q r).aig,
-        (go aig w falseRef trueRef n d w 0 q r).q.get idx hidx,
+        (go aig w n d w 0 q r).aig,
+        (go aig w n d w 0 q r).q.get idx hidx,
         assign
       ⟧
         =
@@ -373,13 +342,11 @@ theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
   · exact hright
   · simp [hq]
   · simp [hr]
-  · exact hfalse
-  · exact htrue
 
-theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
+theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat)
     (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
     ⟦
-      (go aig curr falseRef trueRef n d wn wr q r).aig,
+      (go aig curr n d wn wr q r).aig,
       ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
@@ -414,23 +381,12 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
       rw [hdiscr]
       rw [blastUdiv.go_denote_mem_prefix]
       rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
       rw [denote_blastConst]
       simp
     · intro idx hidx
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-      · simp [hright]
-      · simp [Ref.hgate]
+      simp [hright]
     · intro idx hidx
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      · simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
-        rw [denote_blastConst]
-        simp
-      · simp [Ref.hgate]
+      simp
   · next hdiscr =>
     rw [blastUdiv.go_denote_mem_prefix] at hdiscr
     rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
@@ -440,54 +396,28 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
       rw [blastUdiv.denote_go (hzero := hzero)]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
         · simp [hleft]
         · simp [Ref.hgate]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
         · simp [hright]
         · simp [Ref.hgate]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
         · simp only [RefVec.get_cast, Ref.cast_eq]
           rw [denote_blastConst]
           simp
         · simp [Ref.hgate]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
         · simp only [RefVec.get_cast, Ref.cast_eq]
           rw [denote_blastConst]
           simp
         · simp [Ref.hgate]
-      · rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        · simp
-        · simp [Ref.hgate]
-      · rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        · simp
-        · simp [Ref.hgate]
     · intro idx hdix
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-      · simp [hright]
-      · simp [Ref.hgate]
+      simp [hright]
     · intro idx hdix
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      · simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
-        rw [denote_blastConst]
-        simp
-      · simp [Ref.hgate]
+      simp
 
 end bitblast
 end BVExpr
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
index 1591d5016a..f73321d4ca 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
@@ -35,15 +35,12 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
   · simp
   · dsimp only
     intro idx hidx
-    rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
     rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)]
     apply hleft
   · dsimp only
     intro idx hidx
-    rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-    · simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
-      rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem]
-    · simp [Ref.hgate]
+    simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
+    rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem]
 
 end BVPred
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
index aa0722771f..d6ff0b3fe8 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
@@ -26,18 +26,16 @@ namespace blastUmod
 open blastUdiv
 
 theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
+    (n d q r : AIG.RefVec aig w) (wn wr : Nat)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
     (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
     (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
-    (hfalse : ⟦aig, falseRef, assign⟧ = false)
-    (htrue : ⟦aig, trueRef, assign⟧ = true)
       :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦
-        (go aig curr falseRef trueRef n d wn wr q r).aig,
-        (go aig curr falseRef trueRef n d wn wr q r).r.get idx hidx,
+        (go aig curr n d wn wr q r).aig,
+        (go aig curr n d wn wr q r).r.get idx hidx,
         assign
       ⟧
         =
@@ -69,8 +67,6 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hright
         · exact hq
         · exact hr
-        · exact hfalse
-        · exact htrue
       · intro idx hidx
         rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
         · rw [BitVec.divSubtractShift]
@@ -78,13 +74,6 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hleft
         · exact hright
         · exact hr
-        · exact hfalse
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [hfalse]
-        · simp [Ref.hgate]
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [htrue]
-        · simp [Ref.hgate]
     · next hdiscr =>
       rw [ih]
       · rfl
@@ -104,8 +93,6 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hright
         · exact hq
         · exact hr
-        · exact hfalse
-        · exact htrue
       · intro idx hidx
         rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
         · rw [BitVec.divSubtractShift]
@@ -113,28 +100,19 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
         · exact hleft
         · exact hright
         · exact hr
-        · exact hfalse
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [hfalse]
-        · simp [Ref.hgate]
-      · rw [blastDivSubtractShift_denote_mem_prefix]
-        · simp [htrue]
-        · simp [Ref.hgate]
 
 theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
-    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w)
+    (n d q r : AIG.RefVec aig w)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
     (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = false)
     (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = false)
-    (hfalse : ⟦aig, falseRef, assign⟧ = false)
-    (htrue : ⟦aig, trueRef, assign⟧ = true)
     (hzero : 0#w < rhs)
       :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦
-        (go aig w falseRef trueRef n d w 0 q r).aig,
-        (go aig w falseRef trueRef n d w 0 q r).r.get idx hidx,
+        (go aig w n d w 0 q r).aig,
+        (go aig w n d w 0 q r).r.get idx hidx,
         assign
       ⟧
         =
@@ -147,8 +125,6 @@ theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
   · exact hright
   · simp [hq]
   · simp [hr]
-  · exact hfalse
-  · exact htrue
 
 end blastUmod
 
@@ -172,24 +148,14 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
       rw [hdiscr]
       rw [blastUdiv.go_denote_mem_prefix]
       rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
       · simp [hleft]
       · simp [Ref.hgate]
     · intro idx hidx
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-      · simp [hright]
-      · simp [Ref.hgate]
+      simp [hright]
     · intro idx hidx
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      · simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
-        rw [denote_blastConst]
-        simp
-      · simp [Ref.hgate]
+      simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
+      rw [denote_blastConst]
+      simp
   · next hdiscr =>
     rw [blastUdiv.go_denote_mem_prefix] at hdiscr
     rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
@@ -199,54 +165,28 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
       rw [blastUmod.denote_go (hzero := hzero)]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
         · simp [hleft]
         · simp [Ref.hgate]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
         · simp [hright]
         · simp [Ref.hgate]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
         · simp only [RefVec.get_cast, Ref.cast_eq]
           rw [denote_blastConst]
           simp
         · simp [Ref.hgate]
       · intro idx hidx
         rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
         · simp only [RefVec.get_cast, Ref.cast_eq]
           rw [denote_blastConst]
           simp
         · simp [Ref.hgate]
-      · rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-        · simp
-        · simp [Ref.hgate]
-      · rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
-        · simp
-        · simp [Ref.hgate]
     · intro idx hdix
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-      · simp [hright]
-      · simp [Ref.hgate]
+      simp [hright]
     · intro idx hdix
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-      · simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
-        rw [denote_blastConst]
-        simp
-      · simp [Ref.hgate]
+      simp
 
 end bitblast
 end BVExpr
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
index c148dd8a20..fca880f1f5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
@@ -43,11 +43,6 @@ theorem go_get_aux (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
       intros
       rw [go_get_aux]
       rw [AIG.RefVec.get_push_ref_lt]
-      · simp only [Ref.cast, Ref.mk.injEq]
-        rw [AIG.RefVec.get_cast]
-        · simp
-        · assumption
-      · apply go_le_size
   · dsimp only at hgo
     rw [← hgo]
     simp only [Nat.le_refl, get, Ref.gate_cast, Ref.mk.injEq, true_implies]
@@ -122,7 +117,8 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid
         rw [go_get]
         rw [AIG.RefVec.get_push_ref_eq']
         · rw [go_denote_mem_prefix]
-          · simp [heq]
+          · simp only [Ref.cast_eq]
+            rw [denote_mkConstCached]
           · simp [Ref.hgate]
         · omega
     | inr =>
@@ -132,10 +128,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid
         omega
       · rw [← hgo]
         rw [go_denote_eq]
-        · split
-          · omega
-          · rfl
-        · omega
+        omega
   · omega
 termination_by newWidth - curr
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
index 81511863dc..bfd45e7bc1 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
@@ -64,7 +64,7 @@ theorem bitblast_Inv_of_Inv (input : BVExpr.WithCache BVPred aig)
         exact hinv
   · dsimp only
     apply BVExpr.Cache.Inv_cast
-    · apply AIG.LawfulOperator.isPrefix_aig (f := blastGetLsbD)
+    · apply IsPrefix.rfl
     · apply BVExpr.bitblast_Inv_of_Inv
       exact hinv