diff --git a/Auto/Embedding/LamBase.lean b/Auto/Embedding/LamBase.lean
index ba6fd02..c5ed023 100644
--- a/Auto/Embedding/LamBase.lean
+++ b/Auto/Embedding/LamBase.lean
@@ -958,17 +958,131 @@ def StringConst.lamCheck_of_LamWF (H : LamWF sc s) : sc.lamCheck = s := by
 def StringConst.LamWF.ofCheck (H : sc.lamCheck = s) : LamWF sc s := by
   cases H; cases sc <;> constructor
 
+inductive BVAOp where
+  | add
+  | sub
+  | mul
+  -- `Std.BitVec.smtUDiv`
+  | udiv
+  | urem
+  -- `Std.BitVec.smtSDiv`
+  | sdiv
+  | srem
+  | smod
+  deriving Inhabited, Hashable, Lean.ToExpr
+
+def BVAOp.repr (n : Nat) : BVAOp → String
+| .add  => s!"bvadd {n}"
+| .sub  => s!"bvsub {n}"
+| .mul  => s!"bvmul {n}"
+| .udiv => s!"bvudiv {n}"
+| .urem => s!"bvurem {n}"
+| .sdiv => s!"bvsdiv {n}"
+| .srem => s!"bvsrem {n}"
+| .smod => s!"bvsmod {n}"
+
+def BVAOp.toString : BVAOp → String
+| .add  => s!"+"
+| .sub  => s!"-"
+| .mul  => s!"*"
+| .udiv => s!"/ᵤ"
+| .urem => s!"%ᵤ"
+| .sdiv => s!"/"
+| .srem => s!"%ᵣ"
+| .smod => s!"%"
+
+def BVAOp.beq : BVAOp → BVAOp → Bool
+| add,  add  => true
+| sub,  sub  => true
+| mul,  mul  => true
+| udiv, udiv => true
+| urem, urem => true
+| sdiv, sdiv => true
+| srem, srem => true
+| smod, smod => true
+| _,    _    => false
+
+instance : BEq BVAOp where
+  beq := BVAOp.beq
+
+def BVAOp.beq_refl {a : BVAOp} : (a.beq a) = true := by
+  cases a <;> rfl
+
+def BVAOp.eq_of_beq_eq_true {a₁ a₂ : BVAOp} (H : a₁.beq a₂) : a₁ = a₂ := by
+  cases a₁ <;> cases a₂ <;> first | contradiction | rfl
+
+instance : LawfulBEq BVAOp where
+  eq_of_beq := BVAOp.eq_of_beq_eq_true
+  rfl := BVAOp.beq_refl
+
+inductive BVCmp where
+  | ult
+  | ule
+  | slt
+  | sle
+  deriving Inhabited, Hashable, Lean.ToExpr
+
+def BVCmp.repr (n : Nat) (prop? : Bool) (cmp : BVCmp) : String :=
+  let pStr := if prop? then "p" else ""
+  match cmp with
+  | .ult => s!"bv{pStr}ult {n}"
+  | .ule => s!"bv{pStr}ule {n}"
+  | .slt => s!"bv{pStr}slt {n}"
+  | .sle => s!"bv{pStr}sle {n}"
+
+def BVCmp.toString (prop? : Bool) (cmp : BVCmp) : String :=
+  let pStr := if prop? then "ₚ" else ""
+  match cmp with
+  | .ult => s!"{pStr}<ᵤ"
+  | .ule => s!"{pStr}≤ᵤ"
+  | .slt => s!"{pStr}<"
+  | .sle => s!"{pStr}≤"
+
+def BVCmp.beq : BVCmp → BVCmp → Bool
+| .ult, .ult => true
+| .ule, .ule => true
+| .slt, .slt => true
+| .sle, .sle => true
+| _,    _    => false
+
+instance : BEq BVCmp where
+  beq := BVCmp.beq
+
+def BVCmp.beq_refl {c : BVCmp} : (c.beq c) = true := by
+  cases c <;> rfl
+
+def BVCmp.eq_of_beq_eq_true {c₁ c₂ : BVCmp} (H : c₁.beq c₂) : c₁ = c₂ := by
+  cases c₁ <;> cases c₂ <;> first | contradiction | rfl
+
+instance : LawfulBEq BVCmp where
+  eq_of_beq := BVCmp.eq_of_beq_eq_true
+  rfl := BVCmp.beq_refl
+
 inductive BVShOp where
   | shl
   | lshr
   | ashr
   deriving Inhabited, Hashable, Lean.ToExpr
 
+def BVShOp.repr (n : Nat) (smt? : Bool) (shOp : BVShOp) : String :=
+  let smtStr := if smt? then "smt" else ""
+  match shOp with
+  | .shl  => s!"bv{smtStr}shl {n}"
+  | .lshr => s!"bv{smtStr}lshr {n}"
+  | .ashr => s!"bv{smtStr}ashr {n}"
+
+def BVShOp.toString (smt? : Bool) (shOp : BVShOp) : String :=
+  let smtStr := if smt? then "ₛ" else ""
+  match shOp with
+  | .shl => s!"<<<{smtStr}"
+  | .lshr => s!">>>{smtStr}"
+  | .ashr => s!">>>ₐ{smtStr}"
+
 def BVShOp.beq : BVShOp → BVShOp → Bool
-| shl,         shl         => true
-| lshr,        lshr        => true
-| ashr,        ashr        => true
-| _,           _           => false
+| shl,  shl  => true
+| lshr, lshr => true
+| ashr, ashr => true
+| _,    _    => false
 
 instance : BEq BVShOp where
   beq := BVShOp.beq
@@ -996,22 +1110,10 @@ inductive BitVecConst
   | bvmsb (n : Nat)
   -- zero : Use `bvofNat`
   -- allones : Use `bvneg`
-  | bvadd (n : Nat)
-  | bvsub (n : Nat)
+  | bvaOp (n : Nat) (op : BVAOp)
   | bvneg (n : Nat)
   | bvabs (n : Nat)
-  | bvmul (n : Nat)
-  -- `Std.BitVec.smtUDiv`
-  | bvudiv (n : Nat)
-  | bvurem (n : Nat)
-  -- `Std.BitVec.smtSDiv`
-  | bvsdiv (n : Nat)
-  | bvsrem (n : Nat)
-  | bvsmod (n : Nat)
-  | bvult (n : Nat)
-  | bvule (n : Nat)
-  | bvslt (n : Nat)
-  | bvsle (n : Nat)
+  | bvcmp (n : Nat) (prop? : Bool) (op : BVCmp)
   | bvand (n : Nat)
   | bvor (n : Nat)
   | bvxor (n : Nat)
@@ -1027,6 +1129,38 @@ inductive BitVecConst
   | bvsignExtend (w v : Nat)
 deriving Inhabited, Hashable, Lean.ToExpr
 
+def BitVecConst.bvadd (n : Nat) := BitVecConst.bvaOp n .add
+
+def BitVecConst.bvsub (n : Nat) := BitVecConst.bvaOp n .sub
+
+def BitVecConst.bvmul (n : Nat) := BitVecConst.bvaOp n .mul
+
+def BitVecConst.bvudiv (n : Nat) := BitVecConst.bvaOp n .udiv
+
+def BitVecConst.bvurem (n : Nat) := BitVecConst.bvaOp n .urem
+
+def BitVecConst.bvsdiv (n : Nat) := BitVecConst.bvaOp n .sdiv
+
+def BitVecConst.bvsrem (n : Nat) := BitVecConst.bvaOp n .srem
+
+def BitVecConst.bvsmod (n : Nat) := BitVecConst.bvaOp n .smod
+
+def BitVecConst.bvult (n : Nat) := BitVecConst.bvcmp n false .ult
+
+def BitVecConst.bvule (n : Nat) := BitVecConst.bvcmp n false .ule
+
+def BitVecConst.bvslt (n : Nat) := BitVecConst.bvcmp n false .slt
+
+def BitVecConst.bvsle (n : Nat) := BitVecConst.bvcmp n false .sle
+
+def BitVecConst.bvpropult (n : Nat) := BitVecConst.bvcmp n true .ult
+
+def BitVecConst.bvpropule (n : Nat) := BitVecConst.bvcmp n true .ule
+
+def BitVecConst.bvpropslt (n : Nat) := BitVecConst.bvcmp n true .slt
+
+def BitVecConst.bvpropsle (n : Nat) := BitVecConst.bvcmp n true .sle
+
 def BitVecConst.bvshl (n : Nat) := BitVecConst.bvshOp n false .shl
 
 def BitVecConst.bvlshr (n : Nat) := BitVecConst.bvshOp n false .lshr
@@ -1046,30 +1180,15 @@ def BitVecConst.reprAux : BitVecConst → String
 | .bvofInt n => s!"bvofInt {n}"
 | .bvtoInt n => s!"bvtoInt {n}"
 | .bvmsb n   => s!"bvmsb {n}"
-| .bvadd n   => s!"bvadd {n}"
-| .bvsub n   => s!"bvsub {n}"
+| .bvaOp n op => op.repr n
 | .bvneg n   => s!"bvneg {n}"
 | .bvabs n   => s!"bvabs {n}"
-| .bvmul n   => s!"bvmul {n}"
-| .bvudiv n  => s!"bvudiv {n}"
-| .bvurem n  => s!"bvurem {n}"
-| .bvsdiv n  => s!"bvsdiv {n}"
-| .bvsrem n  => s!"bvsrem {n}"
-| .bvsmod n  => s!"bvsmod {n}"
-| .bvult n   => s!"bvult {n}"
-| .bvule n   => s!"bvule {n}"
-| .bvslt n   => s!"bvslt {n}"
-| .bvsle n   => s!"bvsle {n}"
+| .bvcmp n prop? cmp => cmp.repr n prop?
 | .bvand n   => s!"bvand {n}"
 | .bvor n    => s!"bvor {n}"
 | .bvxor n   => s!"bvxor {n}"
 | .bvnot n   => s!"bvnot {n}"
-| .bvshOp n smt? shOp =>
-  let smtStr := if smt? then "smt" else ""
-  match shOp with
-  | .shl  => s!"bv{smtStr}shl {n}"
-  | .lshr => s!"bv{smtStr}lshr {n}"
-  | .ashr => s!"bv{smtStr}ashr {n}"
+| .bvshOp n smt? shOp => shOp.repr n smt?
 | .bvappend n m      => s!"bvappend {n} {m}"
 | .bvextract n hi lo => s!"bvextract {n} {hi} {lo}"
 | .bvrepeat w i      => s!"bvrepeat {w} {i}"
@@ -1091,30 +1210,15 @@ def BitVecConst.toString : BitVecConst → String
 | .bvofInt n => s!"bvofInt {n}"
 | .bvtoInt n => s!"bvtoInt {n}"
 | .bvmsb n => s!"bvmsb {n}"
-| .bvadd _ => s!"+"
-| .bvsub _ => s!"-"
+| .bvaOp _ op => op.toString
 | .bvneg _ => s!"-"
 | .bvabs _ => s!"bvabs"
-| .bvmul _ => s!"*"
-| .bvudiv _ => s!"/ᵤ"
-| .bvurem _ => s!"%ᵤ"
-| .bvsdiv _ => s!"/"
-| .bvsrem _ => s!"%ᵣ"
-| .bvsmod _ => s!"%"
-| .bvult _ => s!"<ᵤ"
-| .bvule _ => s!"≤ᵤ"
-| .bvslt _ => s!"<"
-| .bvsle _ => s!"≤"
+| .bvcmp _ prop? op => op.toString prop?
 | .bvand _ => s!"&&&"
 | .bvor _ => s!"|||"
 | .bvxor _ => s!"^^^"
 | .bvnot _ => s!"!"
-| .bvshOp _ smt? shOp =>
-  let smtStr := if smt? then "ₛ" else ""
-  match shOp with
-  | .shl => s!"<<<{smtStr}"
-  | .lshr => s!">>>{smtStr}"
-  | .ashr => s!">>>ₐ{smtStr}"
+| .bvshOp _ smt? shOp => shOp.toString smt?
 | .bvappend _ _ => s!"++"
 | .bvextract _ hi lo => s!"bvextract {hi} {lo}"
 | .bvrepeat _ i => s!"bvrepeat {i}"
@@ -1131,20 +1235,10 @@ def BitVecConst.beq : BitVecConst → BitVecConst → Bool
 | .bvofInt n₁,         .bvofInt n₂         => n₁.beq n₂
 | .bvtoInt n₁,         .bvtoInt n₂         => n₁.beq n₂
 | .bvmsb n₁,           .bvmsb n₂           => n₁.beq n₂
-| .bvadd n₁,           .bvadd n₂           => n₁.beq n₂
-| .bvsub n₁,           .bvsub n₂           => n₁.beq n₂
+| .bvaOp n₁ op₁,       .bvaOp n₂ op₂       => n₁.beq n₂ && op₁.beq op₂
 | .bvneg n₁,           .bvneg n₂           => n₁.beq n₂
 | .bvabs n₁,           .bvabs n₂           => n₁.beq n₂
-| .bvmul n₁,           .bvmul n₂           => n₁.beq n₂
-| .bvudiv n₁,          .bvudiv n₂          => n₁.beq n₂
-| .bvurem n₁,          .bvurem n₂          => n₁.beq n₂
-| .bvsdiv n₁,          .bvsdiv n₂          => n₁.beq n₂
-| .bvsrem n₁,          .bvsrem n₂          => n₁.beq n₂
-| .bvsmod n₁,          .bvsmod n₂          => n₁.beq n₂
-| .bvult n₁,           .bvult n₂           => n₁.beq n₂
-| .bvule n₁,           .bvule n₂           => n₁.beq n₂
-| .bvslt n₁,           .bvslt n₂           => n₁.beq n₂
-| .bvsle n₁,           .bvsle n₂           => n₁.beq n₂
+| .bvcmp n₁ prop₁ op₁, .bvcmp n₂ prop₂ op₂ => n₁.beq n₂ && prop₁ == prop₂ && op₁.beq op₂
 | .bvand n₁,           .bvand n₂           => n₁.beq n₂
 | .bvor n₁,            .bvor n₂            => n₁.beq n₂
 | .bvxor n₁,           .bvxor n₂           => n₁.beq n₂
@@ -1163,13 +1257,19 @@ instance : BEq BitVecConst where
 def BitVecConst.beq_refl {b : BitVecConst} : (b.beq b) = true := by
   cases b <;> dsimp [beq] <;> rw [Nat.beq_refl] <;> (try rw [Nat.beq_refl]) <;> (try rfl) <;>
     (try rw [Nat.beq_refl]) <;> (try rfl)
+  case bvaOp => rw [BVAOp.beq_refl]; rfl
+  case bvcmp => rw [LawfulBEq.rfl (α := Bool)]; rw [BVCmp.beq_refl]; rfl
   case bvshOp => rw [LawfulBEq.rfl (α := Bool)]; rw [BVShOp.beq_refl]; rfl
 
 def BitVecConst.eq_of_beq_eq_true {b₁ b₂ : BitVecConst} (H : b₁.beq b₂) : b₁ = b₂ := by
   cases b₁ <;> cases b₂ <;> (try contradiction) <;> (try rw [Nat.eq_of_beq_eq_true H]) <;>
     dsimp [beq] at H <;> rw [Bool.and_eq_true] at H <;> (try rw [Bool.and_eq_true] at H) <;>
     (try rw [Nat.eq_of_beq_eq_true H.right]) <;> (try rw [Nat.eq_of_beq_eq_true H.left]) <;>
-    rw [Nat.eq_of_beq_eq_true H.left.left]
+    (try rw [Nat.eq_of_beq_eq_true H.left.left])
+  case bvaOp.bvaOp =>
+    rw [BVAOp.eq_of_beq_eq_true H.right]
+  case bvcmp.bvcmp =>
+    rw [LawfulBEq.eq_of_beq H.left.right, BVCmp.eq_of_beq_eq_true H.right]
   case bvshOp.bvshOp =>
     rw [LawfulBEq.eq_of_beq H.left.right, BVShOp.eq_of_beq_eq_true H.right]
   case bvextract.bvextract =>
@@ -1186,20 +1286,13 @@ def BitVecConst.lamCheck : BitVecConst → LamSort
 | .bvofInt n        => .func (.base .int) (.base (.bv n))
 | .bvtoInt n        => .func (.base (.bv n)) (.base .int)
 | .bvmsb n          => .func (.base (.bv n)) (.base .bool)
-| .bvadd n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvsub n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
+| .bvaOp n _        => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
 | .bvneg n          => .func (.base (.bv n)) (.base (.bv n))
 | .bvabs n          => .func (.base (.bv n)) (.base (.bv n))
-| .bvmul n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvudiv n         => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvurem n         => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvsdiv n         => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvsrem n         => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvsmod n         => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
-| .bvult n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool))
-| .bvule n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool))
-| .bvslt n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool))
-| .bvsle n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool))
+| .bvcmp n prop? _ =>
+  match prop? with
+  | false => .func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool))
+  | true => .func (.base (.bv n)) (.func (.base (.bv n)) (.base .prop))
 | .bvand n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
 | .bvor n           => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
 | .bvxor n          => .func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n)))
@@ -1221,20 +1314,11 @@ inductive BitVecConst.LamWF : BitVecConst → LamSort → Type
   | ofBvofInt n        : LamWF (.bvofInt n) (.func (.base .int) (.base (.bv n)))
   | ofBvtoInt n        : LamWF (.bvtoInt n) (.func (.base (.bv n)) (.base .int))
   | ofBvmsb n          : LamWF (.bvmsb n) (.func (.base (.bv n)) (.base .bool))
-  | ofBvadd n          : LamWF (.bvadd n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvsub n          : LamWF (.bvsub n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
+  | ofBvaOp n op       : LamWF (.bvaOp n op) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
   | ofBvneg n          : LamWF (.bvneg n) (.func (.base (.bv n)) (.base (.bv n)))
   | ofBvabs n          : LamWF (.bvabs n) (.func (.base (.bv n)) (.base (.bv n)))
-  | ofBvmul n          : LamWF (.bvmul n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvudiv n         : LamWF (.bvudiv n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvurem n         : LamWF (.bvurem n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvsdiv n         : LamWF (.bvsdiv n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvsrem n         : LamWF (.bvsrem n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvsmod n         : LamWF (.bvsmod n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
-  | ofBvult n          : LamWF (.bvult n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)))
-  | ofBvule n          : LamWF (.bvule n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)))
-  | ofBvslt n          : LamWF (.bvslt n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)))
-  | ofBvsle n          : LamWF (.bvsle n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)))
+  | ofBvcmp n op       : LamWF (.bvcmp n false op) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)))
+  | ofBvpropcmp n op   : LamWF (.bvcmp n true op) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base .prop)))
   | ofBvand n          : LamWF (.bvand n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
   | ofBvor n           : LamWF (.bvor n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
   | ofBvxor n          : LamWF (.bvxor n) (.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))))
@@ -1247,6 +1331,38 @@ inductive BitVecConst.LamWF : BitVecConst → LamSort → Type
   | ofBvzeroExtend w v : LamWF (.bvzeroExtend w v) (.func (.base (.bv w)) (.base (.bv v)))
   | ofBvsignExtend w v : LamWF (.bvsignExtend w v) (.func (.base (.bv w)) (.base (.bv v)))
 
+def BitVecConst.LamWF.ofBvadd (n : Nat) := LamWF.ofBvaOp n .add
+
+def BitVecConst.LamWF.ofBvsub (n : Nat) := LamWF.ofBvaOp n .sub
+
+def BitVecConst.LamWF.ofBvmul (n : Nat) := LamWF.ofBvaOp n .mul
+
+def BitVecConst.LamWF.ofBvudiv (n : Nat) := LamWF.ofBvaOp n .udiv
+
+def BitVecConst.LamWF.ofBvurem (n : Nat) := LamWF.ofBvaOp n .urem
+
+def BitVecConst.LamWF.ofBvsdiv (n : Nat) := LamWF.ofBvaOp n .sdiv
+
+def BitVecConst.LamWF.ofBvsrem (n : Nat) := LamWF.ofBvaOp n .srem
+
+def BitVecConst.LamWF.ofBvsmod (n : Nat) := LamWF.ofBvaOp n .smod
+
+def BitVecConst.LamWF.ofBvult (n : Nat) := LamWF.ofBvcmp n .ult
+
+def BitVecConst.LamWF.ofBvule (n : Nat) := LamWF.ofBvcmp n .ule
+
+def BitVecConst.LamWF.ofBvslt (n : Nat) := LamWF.ofBvcmp n .slt
+
+def BitVecConst.LamWF.ofBvsle (n : Nat) := LamWF.ofBvcmp n .sle
+
+def BitVecConst.LamWF.ofBvpropult (n : Nat) := LamWF.ofBvpropcmp n .ult
+
+def BitVecConst.LamWF.ofBvpropule (n : Nat) := LamWF.ofBvpropcmp n .ule
+
+def BitVecConst.LamWF.ofBvpropslt (n : Nat) := LamWF.ofBvpropcmp n .slt
+
+def BitVecConst.LamWF.ofBvpropsle (n : Nat) := LamWF.ofBvpropcmp n .sle
+
 def BitVecConst.LamWF.ofBvshl (n : Nat) := LamWF.ofBvshOp n .shl
 
 def BitVecConst.LamWF.ofBvlshr (n : Nat) := LamWF.ofBvshOp n .lshr
@@ -1270,20 +1386,13 @@ def BitVecConst.LamWF.ofBitVecConst : (b : BitVecConst) → (s : LamSort) × Bit
 | .bvofInt n        => ⟨.func (.base .int) (.base (.bv n)), .ofBvofInt n⟩
 | .bvtoInt n        => ⟨.func (.base (.bv n)) (.base .int), .ofBvtoInt n⟩
 | .bvmsb n          => ⟨.func (.base (.bv n)) (.base .bool), .ofBvmsb n⟩
-| .bvadd n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvadd n⟩
-| .bvsub n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvsub n⟩
+| .bvaOp n op       => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvaOp n op⟩
 | .bvneg n          => ⟨.func (.base (.bv n)) (.base (.bv n)), .ofBvneg n⟩
 | .bvabs n          => ⟨.func (.base (.bv n)) (.base (.bv n)), .ofBvabs n⟩
-| .bvmul n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvmul n⟩
-| .bvudiv n         => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvudiv n⟩
-| .bvurem n         => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvurem n⟩
-| .bvsdiv n         => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvsdiv n⟩
-| .bvsrem n         => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvsrem n⟩
-| .bvsmod n         => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvsmod n⟩
-| .bvult n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)), .ofBvult n⟩
-| .bvule n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)), .ofBvule n⟩
-| .bvslt n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)), .ofBvslt n⟩
-| .bvsle n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)), .ofBvsle n⟩
+| .bvcmp n prop? op =>
+  match prop? with
+  | false => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base .bool)), .ofBvcmp n op⟩
+  | true => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base .prop)), .ofBvpropcmp n op⟩
 | .bvand n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvand n⟩
 | .bvor n           => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvor n⟩
 | .bvxor n          => ⟨.func (.base (.bv n)) (.func (.base (.bv n)) (.base (.bv n))), .ofBvxor n⟩
@@ -1306,6 +1415,7 @@ def BitVecConst.lamCheck_of_LamWF (H : LamWF b s) : b.lamCheck = s := by
 
 def BitVecConst.LamWF.ofCheck (H : b.lamCheck = s) : LamWF b s := by
   cases H; cases b <;> try constructor
+  case bvcmp n prop? op => cases prop? <;> constructor
   case bvshOp n smt? op => cases smt? <;> constructor
 
 /--
@@ -1413,6 +1523,10 @@ def LamBaseTerm.bvult (n : Nat) := LamBaseTerm.bvcst (.bvult n)
 def LamBaseTerm.bvule (n : Nat) := LamBaseTerm.bvcst (.bvule n)
 def LamBaseTerm.bvslt (n : Nat) := LamBaseTerm.bvcst (.bvslt n)
 def LamBaseTerm.bvsle (n : Nat) := LamBaseTerm.bvcst (.bvsle n)
+def LamBaseTerm.bvpropult (n : Nat) := LamBaseTerm.bvcst (.bvpropult n)
+def LamBaseTerm.bvpropule (n : Nat) := LamBaseTerm.bvcst (.bvpropule n)
+def LamBaseTerm.bvpropslt (n : Nat) := LamBaseTerm.bvcst (.bvpropslt n)
+def LamBaseTerm.bvpropsle (n : Nat) := LamBaseTerm.bvcst (.bvpropsle n)
 def LamBaseTerm.bvand (n : Nat) := LamBaseTerm.bvcst (.bvand n)
 def LamBaseTerm.bvor (n : Nat) := LamBaseTerm.bvcst (.bvor n)
 def LamBaseTerm.bvxor (n : Nat) := LamBaseTerm.bvcst (.bvxor n)
@@ -1976,6 +2090,31 @@ def StringConst.interp_equiv (tyVal : Nat → Type u) (scwf : LamWF sc s) :
   HEq (LamWF.interp tyVal scwf) (interp tyVal sc) := by
   cases scwf <;> rfl
 
+def BVAOp.interp (n : Nat) : (op : BVAOp) →
+  GLift.{1, u} (Std.BitVec n) → GLift.{1, u} (Std.BitVec n) → GLift.{1, u} (Std.BitVec n)
+| .add  => bvaddLift n
+| .sub  => bvsubLift n
+| .mul  => bvmulLift n
+| .udiv => bvudivLift n
+| .urem => bvuremLift n
+| .sdiv => bvsdivLift n
+| .srem => bvsremLift n
+| .smod => bvsmodLift n
+
+def BVCmp.interp (n : Nat) : (op : BVCmp) →
+  GLift.{1, u} (Std.BitVec n) → GLift.{1, u} (Std.BitVec n) → GLift.{1, u} Bool
+| .ult => bvultLift n
+| .ule => bvuleLift n
+| .slt => bvsltLift n
+| .sle => bvsleLift n
+
+def BVCmp.propinterp (n : Nat) : (op : BVCmp) →
+  GLift.{1, u} (Std.BitVec n) → GLift.{1, u} (Std.BitVec n) → GLift.{1, u} Prop
+| .ult => bvpropultLift n
+| .ule => bvpropuleLift n
+| .slt => bvpropsltLift n
+| .sle => bvpropsleLift n
+
 def BVShOp.interp (n : Nat) : (op : BVShOp) →
   GLift.{1, u} (Std.BitVec n) → GLift.{1, u} Nat → GLift.{1, u} (Std.BitVec n)
 | .shl         => bvshlLift n
@@ -1989,39 +2128,28 @@ def BVShOp.smtinterp (n : Nat) : (op : BVShOp) →
 | .ashr        => bvsmtashrLift n
 
 def BitVecConst.interp (tyVal : Nat → Type u) : (b : BitVecConst) → b.lamCheck.interp tyVal
-| .bvVal n i        => GLift.up (Std.BitVec.ofNat n i)
-| .bvofNat n        => bvofNatLift n
-| .bvtoNat n        => bvtoNatLift n
-| .bvofInt n        => bvofIntLift n
-| .bvtoInt n        => bvtoIntLift n
-| .bvmsb n          => bvmsbLift n
-| .bvadd n          => bvaddLift n
-| .bvsub n          => bvsubLift n
-| .bvneg n          => bvnegLift n
-| .bvabs n          => bvabsLift n
-| .bvmul n          => bvmulLift n
-| .bvudiv n         => bvudivLift n
-| .bvurem n         => bvuremLift n
-| .bvsdiv n         => bvsdivLift n
-| .bvsrem n         => bvsremLift n
-| .bvsmod n         => bvsmodLift n
-| .bvult n          => bvultLift n
-| .bvule n          => bvuleLift n
-| .bvslt n          => bvsltLift n
-| .bvsle n          => bvsleLift n
-| .bvand n          => bvandLift n
-| .bvor n           => bvorLift n
-| .bvxor n          => bvxorLift n
-| .bvnot n          => bvnotLift n
-| .bvshOp n smt? op =>
-  match smt? with
-  | false => op.interp n
-  | true  => op.smtinterp n
-| .bvappend n m     => bvappendLift n m
-| .bvextract n h l  => bvextractLift n h l
-| .bvrepeat w i     => bvrepeatLift w i
-| .bvzeroExtend w v => bvzeroExtendLift w v
-| .bvsignExtend w v => bvsignExtendLift w v
+| .bvVal n i         => GLift.up (Std.BitVec.ofNat n i)
+| .bvofNat n         => bvofNatLift n
+| .bvtoNat n         => bvtoNatLift n
+| .bvofInt n         => bvofIntLift n
+| .bvtoInt n         => bvtoIntLift n
+| .bvmsb n           => bvmsbLift n
+| .bvaOp n op        => op.interp n
+| .bvneg n           => bvnegLift n
+| .bvabs n           => bvabsLift n
+| .bvcmp n false op  => op.interp n
+| .bvcmp n true op   => op.propinterp n
+| .bvand n           => bvandLift n
+| .bvor n            => bvorLift n
+| .bvxor n           => bvxorLift n
+| .bvnot n           => bvnotLift n
+| .bvshOp n false op => op.interp n
+| .bvshOp n true op  => op.smtinterp n
+| .bvappend n m      => bvappendLift n m
+| .bvextract n h l   => bvextractLift n h l
+| .bvrepeat w i      => bvrepeatLift w i
+| .bvzeroExtend w v  => bvzeroExtendLift w v
+| .bvsignExtend w v  => bvsignExtendLift w v
 
 def BitVecConst.LamWF.interp (tyVal : Nat → Type u) : (lwf : LamWF b s) → s.interp tyVal
 | .ofBvVal n i        => GLift.up (Std.BitVec.ofNat n i)
@@ -2030,20 +2158,11 @@ def BitVecConst.LamWF.interp (tyVal : Nat → Type u) : (lwf : LamWF b s) → s.
 | .ofBvofInt n        => bvofIntLift n
 | .ofBvtoInt n        => bvtoIntLift n
 | .ofBvmsb n          => bvmsbLift n
-| .ofBvadd n          => bvaddLift n
-| .ofBvsub n          => bvsubLift n
+| .ofBvaOp n op       => op.interp n
 | .ofBvneg n          => bvnegLift n
 | .ofBvabs n          => bvabsLift n
-| .ofBvmul n          => bvmulLift n
-| .ofBvudiv n         => bvudivLift n
-| .ofBvurem n         => bvuremLift n
-| .ofBvsdiv n         => bvsdivLift n
-| .ofBvsrem n         => bvsremLift n
-| .ofBvsmod n         => bvsmodLift n
-| .ofBvult n          => bvultLift n
-| .ofBvule n          => bvuleLift n
-| .ofBvslt n          => bvsltLift n
-| .ofBvsle n          => bvsleLift n
+| .ofBvcmp n op       => op.interp n
+| .ofBvpropcmp n op   => op.propinterp n
 | .ofBvand n          => bvandLift n
 | .ofBvor n           => bvorLift n
 | .ofBvxor n          => bvxorLift n
@@ -2343,7 +2462,7 @@ theorem LamTerm.maxLooseBVarSucc.spec (m : Nat) :
 | .app _ t₁ t₂ => by
   dsimp [hasLooseBVarGe, maxLooseBVarSucc];
   rw [Bool.or_eq_true]; rw [spec m t₁]; rw [spec m t₂];
-  simp [Nat.max]; rw [Nat.gt_eq_succ_le]; rw [Nat.gt_eq_succ_le]; rw [Nat.gt_eq_succ_le];
+  simp [Nat.max]; rw [Nat.gt_eq_succ_le, Nat.gt_eq_succ_le, Nat.gt_eq_succ_le];
   rw [Nat.le_max_iff]
 
 def LamTerm.maxEVarSucc : LamTerm → Nat
@@ -2405,6 +2524,14 @@ abbrev LamTerm.bvsge (n : Nat) : LamTerm := .flipApp (.base (.bvsle n)) (.base (
 
 abbrev LamTerm.bvsgt (n : Nat) : LamTerm := .flipApp (.base (.bvslt n)) (.base (.bv n)) (.base (.bv n)) (.base .bool)
 
+abbrev LamTerm.bvpropuge (n : Nat) : LamTerm := .flipApp (.base (.bvpropule n)) (.base (.bv n)) (.base (.bv n)) (.base .bool)
+
+abbrev LamTerm.bvpropugt (n : Nat) : LamTerm := .flipApp (.base (.bvpropult n)) (.base (.bv n)) (.base (.bv n)) (.base .bool)
+
+abbrev LamTerm.bvpropsge (n : Nat) : LamTerm := .flipApp (.base (.bvpropsle n)) (.base (.bv n)) (.base (.bv n)) (.base .bool)
+
+abbrev LamTerm.bvpropsgt (n : Nat) : LamTerm := .flipApp (.base (.bvpropslt n)) (.base (.bv n)) (.base (.bv n)) (.base .bool)
+
 abbrev LamTerm.bvsmtHshl (n m : Nat) : LamTerm :=
   .lam (.base (.bv n)) (.lam (.base (.bv m)) (.app (.base .nat) (.app (.base (.bv n)) (.base (.bvshl n)) (.bvar 1)) (.app (.base (.bv m)) (.base (.bvtoNat m)) (.bvar 0))))
 
diff --git a/Auto/Embedding/LamBitVec.lean b/Auto/Embedding/LamBitVec.lean
index 567bf79..1375efc 100644
--- a/Auto/Embedding/LamBitVec.lean
+++ b/Auto/Embedding/LamBitVec.lean
@@ -47,23 +47,47 @@ namespace BitVec
 
   theorem toNat_shiftLeft {a : Std.BitVec n} (i : Nat) : (a <<< i).toNat = (a.toNat * (2 ^ i)) % (2 ^ n) := by
     rw [shiftLeft_def]; rcases a with ⟨⟨a, isLt⟩⟩
-    dsimp [Std.BitVec.shiftLeft, Std.BitVec.toNat, Std.BitVec.ofNat, Fin.ofNat']
-    rw [Nat.shiftLeft_eq]
+    unfold Std.BitVec.shiftLeft Std.BitVec.toNat Std.BitVec.ofNat Fin.ofNat'
+    dsimp; rw [Nat.shiftLeft_eq]
 
   theorem toNat_ushiftRight {a : Std.BitVec n} (i : Nat) : (a >>> i).toNat = (a.toNat) / (2 ^ i) := by
     rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩
-    dsimp [ushiftRight, Std.BitVec.toNat, Std.BitVec.ofNat, Fin.ofNat']
-    rw [Nat.mod_eq_of_lt, Nat.shiftRight_eq_div_pow]
+    unfold ushiftRight Std.BitVec.toNat Std.BitVec.ofNat Fin.ofNat'
+    dsimp; rw [Nat.mod_eq_of_lt, Nat.shiftRight_eq_div_pow]
     apply Nat.le_trans (Nat.succ_le_succ _) isLt
     rw [Nat.shiftRight_eq_div_pow]; apply Nat.div_le_self
 
-  theorem toNat_zeroExtend {a : Std.BitVec n} (i : Nat) : (a.zeroExtend i).toNat = a.toNat % (2 ^ i) := rfl
+  theorem toNat_zeroExtend' {a : Std.BitVec n} (le : n ≤ m) : (a.zeroExtend' le).toNat = a.toNat := rfl
+
+  theorem toNat_zeroExtend {a : Std.BitVec n} (i : Nat) : (a.zeroExtend i).toNat = a.toNat % (2 ^ i) := by
+    unfold zeroExtend; cases hdec : decide (n ≤ i)
+    case false =>
+      have hnle := of_decide_eq_false hdec
+      rw [Bool.dite_eq_false (proof:=hnle)]; rfl
+    case true =>
+      have hle := of_decide_eq_true hdec
+      rw [Bool.dite_eq_true (proof:=hle), toNat_zeroExtend']
+      rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
+      apply Nat.le_trans isLt; apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hle
 
   theorem toNat_sub (a b : Std.BitVec n) : (a - b).toNat = (a.toNat + (2 ^ n - b.toNat)) % (2 ^ n) := rfl
 
   theorem toNat_neg (a : Std.BitVec n) : (-a).toNat = (2^n - a.toNat) % (2^n) := by
-    rw [neg_def]; dsimp [Std.BitVec.neg]
-    rw [← sub_def, toNat_sub, toNat_ofNat, Nat.zero_mod, Nat.zero_add]
+    rw [neg_def]; unfold Std.BitVec.neg;
+    rw [← sub_def, toNat_sub]; dsimp
+    rw [toNat_ofNat, Nat.zero_mod, Nat.zero_add]
+
+  theorem toNat_and (a b : Std.BitVec n) : (a &&& b).toNat = a.toNat &&& b.toNat := rfl
+
+  theorem toNat_or (a b : Std.BitVec n) : (a ||| b).toNat = a.toNat ||| b.toNat := rfl
+
+  theorem toNat_xor (a b : Std.BitVec n) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := rfl
+
+  theorem toNat_not_aux (a : Std.BitVec n) : (~~~a).toNat = (1 <<< n).pred ^^^ a.toNat := rfl
+
+  theorem toNat_not (a : Std.BitVec n) : (~~~a).toNat = 2 ^ n - 1 - a.toNat := by
+    rw [toNat_not_aux]; rw [Nat.shiftLeft_eq, Nat.one_mul, ← Nat.sub_one, Nat.ones_xor]
+    rcases a with ⟨⟨_, isLt⟩⟩; exact isLt
 
   theorem shiftLeft_ge_length_eq_zero (a : Std.BitVec n) (i : Nat) : i ≥ n → a <<< i = 0#n := by
     intro h; apply eq_of_val_eq; rw [toNat_shiftLeft, toNat_ofNat]; apply Nat.mod_eq_zero_of_dvd
@@ -86,15 +110,17 @@ namespace BitVec
         rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr
         rw [Nat.pred_lt_iff_le (Nat.pow_two_pos _)]
         apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
-      rw [hzero, Nat.zero_mod, Nat.sub_zero]; apply eq_of_val_eq
-      rw [toNat_ofNat, ← neg_def, toNat_neg, toNat_ofNat]
+      rw [hzero]; apply eq_of_val_eq; rw [toNat_not]
+      rw [toNat_ofNat, toNat_neg, toNat_ofNat, Nat.zero_mod, Nat.sub_zero]
       cases n <;> try rfl
-      case succ =>
-        rw [Nat.mod_eq_of_lt (a:=1)]
-        apply @Nat.pow_le_pow_of_le_right 2 (.step .refl) 1 _ (Nat.succ_le_succ (Nat.zero_le _))
+      case succ n =>
+        have hlt : 2 ≤ 2 ^ Nat.succ n := @Nat.pow_le_pow_of_le_right 2 (.step .refl) 1 (.succ n) (Nat.succ_le_succ (Nat.zero_le _))
+        rw [Nat.mod_eq_of_lt (a:=1) hlt]
+        rw [Nat.mod_eq_of_lt]; apply Nat.sub_lt (Nat.le_trans (.step .refl) hlt) .refl
 
   theorem shiftRight_eq_zero_iff (a : Std.BitVec n) (b : Nat) : a >>> b = 0#n ↔ a.toNat < 2 ^ b := by
-    rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩; dsimp [ushiftRight, Std.BitVec.toNat]
+    rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩;
+    unfold ushiftRight; dsimp [Std.BitVec.toNat]
     rw [eq_iff_val_eq, toNat_ofNat, toNat_ofNat, Nat.zero_mod, Nat.shiftRight_eq_div_pow]
     apply Iff.intro <;> intro h
     case mp =>
@@ -107,6 +133,9 @@ namespace BitVec
       case inr h => cases h; rw [Nat.mul_zero] at hdvd; apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mp hdvd
     case mpr => rw [(Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr h]; rfl
 
+  theorem ofNat_toNat (a : Std.BitVec n) : .ofNat m a.toNat = a.zeroExtend m := by
+    apply eq_of_val_eq; rw [toNat_ofNat, toNat_zeroExtend]
+
   theorem ofNat_add (n a b : Nat) : (a + b)#n = a#n + b#n := by
     apply congrArg (f:=Std.BitVec.ofFin); apply Fin.eq_of_val_eq
     dsimp [Fin.ofNat']; rw [Nat.add_mod]; rfl
@@ -286,7 +315,8 @@ theorem LamEquiv.bvofNat_bvtoNat
     (.mkBvofNat m (.mkBvUOp n (.bvtoNat n) t))
     (.app (.base (.bv n)) (.base (.bvzeroExtend n m)) t) :=
   ⟨.mkBvofNat (.mkBvUOp (.ofBvtoNat n) wft),
-   .ofApp _ (.ofBase (.ofBvzeroExtend n m)) wft, fun lctxTerm => rfl⟩
+   .ofApp _ (.ofBase (.ofBvzeroExtend n m)) wft, fun lctxTerm => by
+    apply GLift.down.inj; apply BitVec.ofNat_toNat⟩
 
 theorem LamEquiv.bvofNat_nadd
   (wfa : LamWF lval.toLamTyVal ⟨lctx, a, .base .nat⟩)
diff --git a/Auto/Embedding/LamChecker.lean b/Auto/Embedding/LamChecker.lean
index 9d62fa0..6a65ffc 100644
--- a/Auto/Embedding/LamChecker.lean
+++ b/Auto/Embedding/LamChecker.lean
@@ -3,8 +3,7 @@ import Auto.Embedding.LamConv
 import Auto.Embedding.LamInference
 import Auto.Embedding.LamLCtx
 import Auto.Embedding.LamPrep
--- Temporarily removing this input until I can get this file to build on Lean v4.4.0-rc1
--- import Auto.Embedding.BitVec
+import Auto.Embedding.LamBitVec
 import Auto.Embedding.LamInductive
 import Auto.Lib.BinTree
 open Lean
@@ -602,10 +601,8 @@ inductive PrepConvStep where
   | validOfPropEq : PrepConvStep
   /-- (a = b) ↔ (a ∨ b) ∧ (¬ a ∨ ¬ b) -/
   | validOfPropNe : PrepConvStep
-  /- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
   /-- Basic BitVec simplification operations -/
   | validOfPushBVCast : PrepConvStep
-  -/
   deriving Inhabited, Hashable, BEq, Lean.ToExpr
 
 inductive WFStep where
@@ -706,9 +703,7 @@ def PrepConvStep.toString : PrepConvStep → String
 | .validOfNotImpEquivAndNot => s!"validOfNotImpEquivAndNot"
 | .validOfPropEq => s!"validOfPropEq"
 | .validOfPropNe => s!"validOfPropNe"
-/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
 | .validOfPushBVCast => s!"validOfPushBVCast"
--/
 
 def WFStep.toString : WFStep → String
 | .wfOfCheck lctx t => s!"wfOfCheck {lctx} {t}"
@@ -1150,9 +1145,7 @@ def InferenceStep.evalValidOfBVarLowers (r : RTable) (lctx : List LamSort) (pns
 | .validOfNotImpEquivAndNot => LamTerm.not_imp_equiv_and_not?
 | .validOfPropEq => LamTerm.propeq?
 | .validOfPropNe => LamTerm.propne?
-/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
 | .validOfPushBVCast => fun t => LamTerm.pushBVCast .none t
--/
 
 @[reducible] def WFStep.eval (lvt lit : Nat → LamSort) (r : RTable) : (cs : WFStep) → EvalResult
 | .wfOfCheck lctx t =>
@@ -2117,11 +2110,9 @@ theorem PrepConvStep.eval_correct (lval : LamValuation) :
 | .validOfPropNe => And.intro
   LamGenConv.propne?
   (LamTerm.evarBounded_of_evarEquiv @LamTerm.maxEVarSucc_propne?)
-/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
 | .validOfPushBVCast => And.intro
   LamGenConv.pushBVCast
   (LamTerm.evarBounded_of_evarEquiv LamTerm.evarEquiv_pushBVCast)
--/
 
 theorem WFStep.eval_correct
   (r : RTable) (cv : CVal.{u} r.lamEVarTy) (inv : r.inv cv) :
@@ -2339,7 +2330,7 @@ theorem Checker.getValidExport_indirectReduceAux
     apply congrFun; apply congrArg; rw [hlit, BinTree.get?_mapOpt]
     apply Eq.symm; apply Option.map_eq_bind
   rw [lvtEq, litEq] at runEq; cases runEq; apply ChkSteps.run_correct
-  dsimp [RTable.inv, BinTree.get?]
+  unfold RTable.inv BinTree.get?
   exists fun _ => BinTree.get?'_leaf _ ▸ GLift.up False
   cases hImport; apply ImportTable.importFacts_correct
 
diff --git a/Auto/Embedding/Lift.lean b/Auto/Embedding/Lift.lean
index d55dc0c..87c75ed 100644
--- a/Auto/Embedding/Lift.lean
+++ b/Auto/Embedding/Lift.lean
@@ -185,6 +185,18 @@ def bvsltLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} B
 def bvsleLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Bool :=
   GLift.up (Std.BitVec.sle x.down y.down)
 
+def bvpropultLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toFin < y.down.toFin)
+
+def bvpropuleLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toFin <= y.down.toFin)
+
+def bvpropsltLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toInt < y.down.toInt)
+
+def bvpropsleLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toInt <= y.down.toInt)
+
 def bvandLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} (Std.BitVec n) :=
   GLift.up (Std.BitVec.and x.down y.down)
 
diff --git a/Auto/Lib/BinTree.lean b/Auto/Lib/BinTree.lean
index 2130e53..090aec8 100644
--- a/Auto/Lib/BinTree.lean
+++ b/Auto/Lib/BinTree.lean
@@ -432,7 +432,7 @@ theorem allp'_node (p : α → Prop) :
         have h' := h (2 * n + 5)
         rw [get?'_succSucc] at h'
         have eq₁ : (2 * n + 5) % 2 = 1 := by
-          rw [Nat.add_mod]; simp; rfl
+          simp [Nat.add_mod]; rfl
         have eq₂ : (2 * n + 5) / 2 = n + 2 := by
           rw [Nat.add_comm _ 5];
           rw [Nat.add_mul_div_left];
diff --git a/Auto/Lib/BoolExtra.lean b/Auto/Lib/BoolExtra.lean
index ef6c0e1..e73ed4b 100644
--- a/Auto/Lib/BoolExtra.lean
+++ b/Auto/Lib/BoolExtra.lean
@@ -15,7 +15,7 @@ theorem Bool.eq_false_of_ne_true {a : Bool} : a ≠ true → a = false := by
 theorem Bool.ne_true_of_eq_false {a : Bool} : a = false → a ≠ true := by
   cases a <;> decide
 
-theorem Bool.eq_false_eq_not_eq_true {a : Bool} : (a ≠ true) = (a = false) := by
+theorem Bool.eq_false_eq_not_eq_true {a : Bool} : (a = false) = (a ≠ true) := by
   cases a <;> decide
 
 theorem Bool.and_eq_false (a b : Bool) : ((a && b) = false) = ((a = false) ∨ (b = false)) := by
@@ -53,6 +53,16 @@ theorem Bool.ite_eq_false (p : Prop) [inst : Decidable p] (a b : α) : ¬ p →
   case isFalse _ => rfl
   case isTrue hp => apply False.elim (hnp hp)
 
+theorem Bool.dite_eq_true (p : Prop) [inst : Decidable p] (a : p → α) (b : ¬ p → α) (proof : p) : dite p a b = a proof := by
+  dsimp [dite]; cases inst
+  case isFalse hnp => apply False.elim (hnp proof)
+  case isTrue _ => rfl
+
+theorem Bool.dite_eq_false (p : Prop) [inst : Decidable p] (a : p → α) (b : ¬ p → α) (proof : ¬ p) : dite p a b = b proof := by
+  dsimp [dite]; cases inst
+  case isFalse _ => rfl
+  case isTrue hp => apply False.elim (proof hp)
+
 /--
   Similar to `ite`, but does not have complicated dependent types
 -/
diff --git a/Auto/Lib/NatExtra.lean b/Auto/Lib/NatExtra.lean
index 7efd0ea..abd6b31 100644
--- a/Auto/Lib/NatExtra.lean
+++ b/Auto/Lib/NatExtra.lean
@@ -1,4 +1,6 @@
 import Std.Data.Nat.Lemmas
+import Std.Data.Nat.Bitwise
+import Auto.Lib.BoolExtra
 
 namespace Auto
 
@@ -86,6 +88,8 @@ theorem Nat.le_max_iff (m n k : Nat) : k ≤ max m n ↔ k ≤ m ∨ k ≤ n :=
     case inl h => exact Nat.le_trans h (Nat.le_max_left _ _)
     case inr h => exact Nat.le_trans h (Nat.le_max_right _ _)
 
+theorem Nat.lt_eq_succ_le {m n : Nat} : n < m ↔ .succ n ≤ m := by rfl
+
 theorem Nat.gt_eq_succ_le {m n : Nat} : m > n ↔ .succ n ≤ m := by rfl
 
 theorem Nat.le_pred_of_succ_le {n m : Nat} : m > 0 → Nat.succ n ≤ m → n ≤ Nat.pred m :=
@@ -109,8 +113,8 @@ theorem Nat.max_add {a b c : Nat} : max a b + c = max (a + c) (b + c) := by
     simp [h, naleb]
 
 theorem Nat.max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
-  rw [← Nat.lt_eq, Nat.lt]; dsimp only [Nat.le_eq]; rw [← Nat.add_one];
-  rw [Nat.max_add]; rw [Nat.max_le]; apply Iff.intro id id
+  rw [show (max a b < c ↔ max a b + 1 ≤ c) by rfl, Nat.max_add, Nat.max_le]
+  apply Iff.intro id id
 
 theorem Nat.max_zero_left {a : Nat} : max 0 a = a := by
   rw [Nat.max_def]; simp
@@ -176,4 +180,122 @@ theorem Nat.le_pow (h : b ≥ 2) : a < b ^ a := by
     rw [Nat.mul_two, Nat.succ_add]
     apply Nat.succ_le_succ; apply Nat.succ_le_succ; apply Nat.le_add_left
 
+  theorem Nat.mod_par {a b c : Nat} (h : a % b = c) : ∃ d, a = b * d + c := by
+    exists (a / b); rw [← h, Nat.div_add_mod]
+
+  theorem Nat.div_par {a b c : Nat} (h : a / b = c) (hnz : b > 0) : ∃ d, a = b * c + d ∧ d < b := by
+    exists (a % b); rw [← h, Nat.div_add_mod]; apply And.intro rfl; apply Nat.mod_lt _ hnz
+
+  theorem Nat.le_par {a b : Nat} (h : a ≤ b) : ∃ c, b = a + c := by
+    exists (b - a); rw [Nat.add_comm, Nat.sub_add_cancel h]
+
+  theorem Nat.lt_par {a b : Nat} (h : a < b) : ∃ c, b = (a + 1) + c := Nat.le_par h
+
+  theorem Nat.sub_mod (a b n : Nat) (h : a ≥ b) : (a - b) % n = (a - b % n) % n := by
+    have ⟨k, hk⟩ := Nat.le_par h
+    generalize hl : b % n = l; have ⟨d, hd⟩ := Nat.mod_par hl
+    have llb : l ≤ b := by rw [← hl]; apply Nat.mod_le
+    have lla : l ≤ a := Nat.le_trans llb h
+    cases hd; rw [Nat.add_comm, Nat.sub_add_eq, Nat.sub_mul_mod]
+    rw [Nat.le_sub_iff_add_le lla]; apply h
+
+  theorem Nat.testBit_true_iff (a i : Nat) : a.testBit i ↔ 2 ^ i ≤ a % 2 ^ (i + 1) := by
+    rw [Nat.testBit_to_div_mod, decide_eq_true_iff]; apply Iff.intro <;> intro h
+    case mp =>
+      have ⟨k, hk⟩ := Nat.mod_par h; clear h
+      have ⟨r, ⟨er, lr⟩⟩ := Nat.div_par hk (Nat.pow_two_pos _); clear hk; cases er
+      have eqi : 2 ^ i * (2 * k + 1) + r = 2 ^ (i + 1) * k + (2 ^ i + r) := by
+        rw [Nat.mul_add _ _ 1, ← Nat.mul_assoc, Nat.pow_add, Nat.add_assoc]; simp
+      rw [eqi, Nat.mul_add_mod]
+      have elt : 2 ^ i + r < 2 ^ (i + 1) := by
+        rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two]
+        rw [Nat.add_lt_add_iff_left]; apply lr
+      rw [Nat.mod_eq_of_lt elt]; apply Nat.le_add_right
+    case mpr =>
+      generalize ek : a % 2 ^ (i + 1) = k at h
+      have lk : k < 2 ^ (i + 1) := by cases ek; apply Nat.mod_lt; apply Nat.pow_two_pos
+      have ⟨l, hl⟩ := Nat.mod_par ek; clear ek; cases hl
+      have eqi : 2 ^ (i + 1) * l + k = 2 ^ i * (2 * l) + k := by
+        rw [Nat.pow_add, Nat.mul_assoc]; simp
+      rw [eqi, Nat.mul_add_div (Nat.pow_two_pos _), Nat.mul_add_mod]
+      have kdge : k / (2 ^ i) > 0 := (Nat.le_div_iff_mul_le (Nat.pow_two_pos _)).mpr (by simp [h])
+      have kdle : k / (2 ^ i) < 2 := (Nat.div_lt_iff_lt_mul (Nat.pow_two_pos _)).mpr (by rw [Nat.pow_add, Nat.mul_comm] at lk; apply lk)
+      have kone : k / (2 ^ i) = 1 := Nat.eq_iff_le_and_ge.mpr (And.intro (Nat.le_of_succ_le_succ kdle) kdge)
+      rw [kone]; rfl
+
+  theorem Nat.testBit_false_iff (a i : Nat) : a.testBit i = false ↔ a % 2 ^ (i + 1) < 2 ^ i := by
+    rw [Bool.eq_false_eq_not_eq_true, ne_eq, Nat.testBit_true_iff, Nat.not_le]
+
+  theorem Nat.ones_testBit_true_of_lt (n i : Nat) (h : i < n) : (2 ^ n - 1).testBit i := by
+    rw [Nat.testBit_true_iff]; have ⟨k, ek⟩ := Nat.lt_par h; clear h; cases ek
+    have eqi : 2 ^ (i + 1 + k) - 1 = 2 ^ (i + 1) * (2 ^ k - 1) + (2 ^ (i + 1) - 1) := calc
+      _ = 2 ^ (i + 1) * 2 ^ k - 1 := by rw [Nat.pow_add]
+      _ = 2 ^ (i + 1) * (2 ^ k - 1 + 1) - 1 := by rw [Nat.sub_add_cancel]; apply Nat.pow_two_pos
+      _ = _ := by
+        have hle : 1 ≤ 2 ^ (i + 1) * 1 := by rw [Nat.mul_one]; apply Nat.pow_two_pos
+        rw [Nat.mul_add]; rw [Nat.add_sub_assoc hle]; simp
+    rw [eqi, Nat.mul_add_mod, Nat.mod_eq_of_lt (Nat.sub_lt (Nat.pow_two_pos _) .refl)]
+    rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two, show (Nat.succ 0 = 1) by rfl]
+    rw [Nat.add_sub_assoc (Nat.pow_two_pos _)]; apply Nat.le_add_right
+
+  theorem Nat.ones_testBit_false_of_ge (n i : Nat) (h : i ≥ n) : (2 ^ n - 1).testBit i = false := by
+    have hl : 2 ^ n - 1 < 2 ^ i := by
+      rw [Nat.lt_eq_succ_le, Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.pow_two_pos _)]
+      apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) h
+    have hls : 2 ^ i ≤ 2 ^ (i + 1) := Nat.pow_le_pow_of_le_right (Nat.le_step .refl) (Nat.le_add_right _ _)
+    rw [Nat.testBit_false_iff]; rw [Nat.mod_eq_of_lt (Nat.le_trans hl hls)]; apply hl
+
+  theorem Nat.xor_def (a b : Nat) : a ^^^ b = a.xor b := rfl
+
+  theorem Nat.ones_xor (n a : Nat) (h : a < 2 ^ n) : (2 ^ n - 1) ^^^ a = 2 ^ n - 1 - a := by
+    apply Nat.eq_of_testBit_eq; intro i
+    rw [xor_def, Nat.xor, Nat.testBit_bitwise (f:=bne) rfl]
+    have texp : 2 ^ (i + 1) = 2 ^ i + 2 ^ i := by rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two]
+    cases @Nat.dichotomy n i
+    case inl hl =>
+      rw [Nat.ones_testBit_false_of_ge _ _ hl]
+      rw [show (∀ b, (false != b) = b) by (intro b; simp)]
+      have ple : 2 ^ n ≤ 2 ^ i := Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hl
+      have lf : Nat.testBit a i = false := by
+        rw [Nat.testBit_false_iff]
+        apply Nat.le_trans _ (Nat.le_trans h ple); apply Nat.succ_le_succ
+        apply Nat.mod_le
+      have rf : Nat.testBit (2 ^ n - 1 - a) i = false := by
+        rw [Nat.testBit_false_iff]
+        have li : 2 ^ n - 1 - a < 2 ^ i := by
+          rw [← Nat.sub_add_eq, Nat.lt_eq_succ_le, Nat.succ_eq_add_one]
+          rw [← Nat.sub_add_comm (show 1 + a ≤ 2 ^ n by rw [Nat.add_comm]; exact h)]
+          rw [Nat.sub_add_eq, Nat.add_sub_cancel]; rw [Nat.sub_le_iff_le_add]
+          apply Nat.le_trans ple (Nat.le_add_right _ _)
+        rw [Nat.mod_eq_of_lt (Nat.le_trans li (by rw [texp]; apply Nat.le_add_right))]
+        apply li
+      rw [lf, rf]
+    case inr hl =>
+      rw [Nat.ones_testBit_true_of_lt _ _ hl]
+      rw [show (∀ b, (true != b) = !b) by (intro b; simp)]
+      generalize hk : a % 2 ^ (i + 1) = k
+      have kl : k < 2 ^ (i + 1) := by rw [← hk]; apply Nat.mod_lt; apply Nat.pow_two_pos
+      have tr : (2 ^ n - 1 - a) % 2 ^ (i + 1) = 2 ^ (i + 1) - (k + 1) := by
+        rw [Nat.sub_mod _ _ _ (show a ≤ 2 ^ n - 1 by exact (Nat.le_sub_iff_add_le (Nat.pow_two_pos _)).mpr h)]
+        rw [hk]; have ⟨dn, hdn⟩ := Nat.lt_par hl; cases hdn
+        rw [Nat.pow_add _ _ dn, show (2 ^ dn = 2 ^ dn - 1 + 1) by rw[Nat.sub_add_cancel (Nat.pow_two_pos _)]]
+        rw [Nat.mul_add, Nat.mul_one, ← Nat.sub_add_eq]
+        rw [Nat.add_sub_assoc (by rw [Nat.add_comm]; exact kl)]
+        rw [Nat.mul_add_mod, Nat.mod_eq_of_lt, Nat.add_comm 1 k]
+        apply Nat.sub_lt (Nat.pow_two_pos _)
+        rw [Nat.add_comm]; apply Nat.zero_lt_succ
+      cases hai : Nat.testBit a i
+      case false =>
+        rw [Nat.testBit_false_iff] at hai
+        apply Eq.symm; rw [show ((!false) = true) by rfl, Nat.testBit_true_iff]
+        rw [hk] at hai; rw [tr, Nat.le_sub_iff_add_le kl, Nat.succ_eq_add_one]
+        rw [texp]; apply Nat.add_le_add_left; exact hai
+      case true =>
+        rw [Nat.testBit_true_iff] at hai
+        apply Eq.symm; rw [show ((!true) = false) by rfl, Nat.testBit_false_iff]
+        rw [hk] at hai; rw [tr, Nat.lt_eq_succ_le, Nat.succ_eq_add_one]
+        rw [← Nat.sub_add_comm kl, Nat.succ_eq_add_one]
+        rw [Nat.add_comm k 1, Nat.sub_add_eq, Nat.add_sub_cancel]
+        rw [Nat.sub_le_iff_le_add, texp]; apply Nat.add_le_add_left; exact hai
+
 end Auto
diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean
index 3e9c303..9b4ae9f 100644
--- a/Auto/Lib/Pos.lean
+++ b/Auto/Lib/Pos.lean
@@ -118,7 +118,7 @@ theorem ofNat'WF_toNat' (p : Pos) : ofNat'WF (toNat' p) = p := by
 theorem toNat'_ofNat'WF (n : Nat) : n ≠ 0 → toNat' (ofNat'WF n) = n := by
   revert n; apply ofNat'WF.induction
   case base₀ => intro H; contradiction
-  case base₁ => intro H; rfl
+  case base₁ => intro _; rfl
   case ind =>
     intro x IH _
     have hne : (x + 2) / 2 ≠ 0 := by
diff --git a/Auto/Translation/Lam2D.lean b/Auto/Translation/Lam2D.lean
index c347a4d..a74581e 100644
--- a/Auto/Translation/Lam2D.lean
+++ b/Auto/Translation/Lam2D.lean
@@ -197,20 +197,32 @@ def interpBitVecConstAsUnlifted : BitVecConst → Expr
 | .bvofInt n         => .app (.const ``Std.BitVec.ofInt []) (.lit (.natVal n))
 | .bvtoInt n         => .app (.const ``Std.BitVec.toInt []) (.lit (.natVal n))
 | .bvmsb n           => .app (.const ``Std.BitVec.msb []) (.lit (.natVal n))
-| .bvadd n           => .app (.const ``Std.BitVec.add []) (.lit (.natVal n))
-| .bvsub n           => .app (.const ``Std.BitVec.sub []) (.lit (.natVal n))
+| .bvaOp n op =>
+  match op with
+  | .add             => .app (.const ``Std.BitVec.add []) (.lit (.natVal n))
+  | .sub             => .app (.const ``Std.BitVec.sub []) (.lit (.natVal n))
+  | .mul             => .app (.const ``Std.BitVec.mul []) (.lit (.natVal n))
+  | .udiv            => .app (.const ``Std.BitVec.smtUDiv []) (.lit (.natVal n))
+  | .urem            => .app (.const ``Std.BitVec.umod []) (.lit (.natVal n))
+  | .sdiv            => .app (.const ``Std.BitVec.smtSDiv []) (.lit (.natVal n))
+  | .srem            => .app (.const ``Std.BitVec.srem []) (.lit (.natVal n))
+  | .smod            => .app (.const ``Std.BitVec.smod []) (.lit (.natVal n))
 | .bvneg n           => .app (.const ``Std.BitVec.neg []) (.lit (.natVal n))
 | .bvabs n           => .app (.const ``Std.BitVec.abs []) (.lit (.natVal n))
-| .bvmul n           => .app (.const ``Std.BitVec.mul []) (.lit (.natVal n))
-| .bvudiv n          => .app (.const ``Std.BitVec.smtUDiv []) (.lit (.natVal n))
-| .bvurem n          => .app (.const ``Std.BitVec.umod []) (.lit (.natVal n))
-| .bvsdiv n          => .app (.const ``Std.BitVec.smtSDiv []) (.lit (.natVal n))
-| .bvsrem n          => .app (.const ``Std.BitVec.srem []) (.lit (.natVal n))
-| .bvsmod n          => .app (.const ``Std.BitVec.smod []) (.lit (.natVal n))
-| .bvult n           => .app (.const ``Std.BitVec.ult []) (.lit (.natVal n))
-| .bvule n           => .app (.const ``Std.BitVec.ule []) (.lit (.natVal n))
-| .bvslt n           => .app (.const ``Std.BitVec.slt []) (.lit (.natVal n))
-| .bvsle n           => .app (.const ``Std.BitVec.sle []) (.lit (.natVal n))
+| .bvcmp n prop? op  =>
+  match prop? with
+  | false =>
+    match op with
+    | .ult           => .app (.const ``Std.BitVec.ult []) (.lit (.natVal n))
+    | .ule           => .app (.const ``Std.BitVec.ule []) (.lit (.natVal n))
+    | .slt           => .app (.const ``Std.BitVec.slt []) (.lit (.natVal n))
+    | .sle           => .app (.const ``Std.BitVec.sle []) (.lit (.natVal n))
+  | true =>
+    match op with
+    | .ult           => .app (.const ``BitVec.propult []) (.lit (.natVal n))
+    | .ule           => .app (.const ``BitVec.propule []) (.lit (.natVal n))
+    | .slt           => .app (.const ``BitVec.propslt []) (.lit (.natVal n))
+    | .sle           => .app (.const ``BitVec.propsle []) (.lit (.natVal n))
 | .bvand n           => .app (.const ``Std.BitVec.and []) (.lit (.natVal n))
 | .bvor n            => .app (.const ``Std.BitVec.or []) (.lit (.natVal n))
 | .bvxor n           => .app (.const ``Std.BitVec.xor []) (.lit (.natVal n))
diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean
index db79315..f18950c 100644
--- a/Auto/Translation/LamFOL2SMT.lean
+++ b/Auto/Translation/LamFOL2SMT.lean
@@ -135,18 +135,22 @@ private def lamBaseTerm2STerm_Arity2 (arg1 arg2 : STerm) : LamBaseTerm → Trans
 | .scst .sle  => return .qStrApp "str.<=" #[arg1, arg2]
 | .scst .slt  => return .qStrApp "str.<" #[arg1, arg2]
 | .scst .sprefixof => return .qStrApp "str.prefixof" #[arg1, arg2]
-| .bvcst (.bvadd _) => return .qStrApp "bvadd" #[arg1, arg2]
-| .bvcst (.bvsub _) => return .qStrApp "bvadd" #[arg1, .qStrApp "bvneg" #[arg2]]
-| .bvcst (.bvmul _) => return .qStrApp "bvmul" #[arg1, arg2]
-| .bvcst (.bvudiv _) => return .qStrApp "bvudiv" #[arg1, arg2]
-| .bvcst (.bvurem _) => return .qStrApp "bvurem" #[arg1, arg2]
-| .bvcst (.bvsdiv _) => return .qStrApp "bvsdiv" #[arg1, arg2]
-| .bvcst (.bvsrem _) => return .qStrApp "bvsrem" #[arg1, arg2]
-| .bvcst (.bvsmod _) => return .qStrApp "bvsmod" #[arg1, arg2]
-| .bvcst (.bvult _) => return .qStrApp "bvult" #[arg1, arg2]
-| .bvcst (.bvule _) => return .qStrApp "bvule" #[arg1, arg2]
-| .bvcst (.bvslt _) => return .qStrApp "bvslt" #[arg1, arg2]
-| .bvcst (.bvsle _) => return .qStrApp "bvsle" #[arg1, arg2]
+| .bvcst (.bvaOp _ op) =>
+  match op with
+  | .add => return .qStrApp "bvadd" #[arg1, arg2]
+  | .sub => return .qStrApp "bvadd" #[arg1, .qStrApp "bvneg" #[arg2]]
+  | .mul => return .qStrApp "bvmul" #[arg1, arg2]
+  | .udiv => return .qStrApp "bvudiv" #[arg1, arg2]
+  | .urem => return .qStrApp "bvurem" #[arg1, arg2]
+  | .sdiv => return .qStrApp "bvsdiv" #[arg1, arg2]
+  | .srem => return .qStrApp "bvsrem" #[arg1, arg2]
+  | .smod => return .qStrApp "bvsmod" #[arg1, arg2]
+| .bvcst (.bvcmp _ _ op) =>
+  match op with
+  | .ult => return .qStrApp "bvult" #[arg1, arg2]
+  | .ule => return .qStrApp "bvule" #[arg1, arg2]
+  | .slt => return .qStrApp "bvslt" #[arg1, arg2]
+  | .sle => return .qStrApp "bvsle" #[arg1, arg2]
 | .bvcst (.bvand _) => return .qStrApp "bvand" #[arg1, arg2]
 | .bvcst (.bvor _) => return .qStrApp "bvor" #[arg1, arg2]
 | .bvcst (.bvxor _) => return .qStrApp "bvxor" #[arg1, arg2]
diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean
index fe1d0f5..a869fc5 100644
--- a/Auto/Translation/LamReif.lean
+++ b/Auto/Translation/LamReif.lean
@@ -1050,9 +1050,7 @@ section CheckerUtils
       else
         return (vs, minds))
     let vs ← vs.mapM validOfBetaReduce
-    /- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
     let vs ← vs.mapM (fun re => validOfPrepConv .validOfPushBVCast re [])
-    -/
     let vs ← vs.mapM validOfRevertAll
     for v in vs do
       trace[auto.lamReif.prep.printResult] "{v}"
@@ -1160,6 +1158,14 @@ abbrev BitVec.uge (a b : Std.BitVec n) : Bool := Std.BitVec.ule b a
 abbrev BitVec.ugt (a b : Std.BitVec n) : Bool := Std.BitVec.ult b a
 abbrev BitVec.sge (a b : Std.BitVec n) : Bool := Std.BitVec.sle b a
 abbrev BitVec.sgt (a b : Std.BitVec n) : Bool := Std.BitVec.slt b a
+abbrev BitVec.propule (a b : Std.BitVec n) : Prop := a.toFin <= b.toFin
+abbrev BitVec.propult (a b : Std.BitVec n) : Prop := a.toFin < b.toFin
+abbrev BitVec.propsle (a b : Std.BitVec n) : Prop := a.toInt <= b.toInt
+abbrev BitVec.propslt (a b : Std.BitVec n) : Prop := a.toInt < b.toInt
+abbrev BitVec.propuge (a b : Std.BitVec n) : Prop := BitVec.propule b a
+abbrev BitVec.propugt (a b : Std.BitVec n) : Prop := BitVec.propult b a
+abbrev BitVec.propsge (a b : Std.BitVec n) : Prop := BitVec.propsle b a
+abbrev BitVec.propsgt (a b : Std.BitVec n) : Prop := BitVec.propslt b a
 abbrev BitVec.smtHshiftLeft (a : Std.BitVec n) (b : Std.BitVec m) := Std.BitVec.shiftLeft a b.toNat
 abbrev BitVec.smtHushiftRight (a : Std.BitVec n) (b : Std.BitVec m) := Std.BitVec.ushiftRight a b.toNat
 abbrev BitVec.smtHsshiftRight (a : Std.BitVec n) (b : Std.BitVec m) := Std.BitVec.sshiftRight a b.toNat
@@ -1358,17 +1364,17 @@ def reifMapLam0Arg2Natlit : HashMap (Name × Name) (Array ((Nat → Expr) × (Na
     ((``Complement.complement, ``Std.BitVec),
               #[(fun n => .app (.const ``Std.BitVec.not []) (.lit (.natVal n)), fun n => .base (.bvnot n))]),
     ((``LE.le, ``Std.BitVec),
-              #[(fun n => .app (.const ``Std.BitVec.ule []) (.lit (.natVal n)), fun n => .base (.bvule n)),
-                (fun n => .app (.const ``Std.BitVec.sle []) (.lit (.natVal n)), fun n => .base (.bvsle n))]),
+              #[(fun n => .app (.const ``BitVec.propule []) (.lit (.natVal n)), fun n => .base (.bvpropule n)),
+                (fun n => .app (.const ``BitVec.propsle []) (.lit (.natVal n)), fun n => .base (.bvpropsle n))]),
     ((``GE.ge, ``Std.BitVec),
-              #[(fun n => .app (.const ``BitVec.uge []) (.lit (.natVal n)), fun n => .bvuge n),
-                (fun n => .app (.const ``BitVec.sge []) (.lit (.natVal n)), fun n => .bvsge n)]),
+              #[(fun n => .app (.const ``BitVec.propuge []) (.lit (.natVal n)), fun n => .bvpropuge n),
+                (fun n => .app (.const ``BitVec.propsge []) (.lit (.natVal n)), fun n => .bvpropsge n)]),
     ((``LT.lt, ``Std.BitVec),
-              #[(fun n => .app (.const ``Std.BitVec.ult []) (.lit (.natVal n)), fun n => .base (.bvult n)),
-                (fun n => .app (.const ``Std.BitVec.slt []) (.lit (.natVal n)), fun n => .base (.bvslt n))]),
+              #[(fun n => .app (.const ``BitVec.propult []) (.lit (.natVal n)), fun n => .base (.bvpropult n)),
+                (fun n => .app (.const ``BitVec.propslt []) (.lit (.natVal n)), fun n => .base (.bvpropslt n))]),
     ((``GT.gt, ``Std.BitVec),
-              #[(fun n => .app (.const ``BitVec.ugt []) (.lit (.natVal n)), fun n => .bvugt n),
-                (fun n => .app (.const ``BitVec.sgt []) (.lit (.natVal n)), fun n => .bvsgt n)])
+              #[(fun n => .app (.const ``BitVec.propugt []) (.lit (.natVal n)), fun n => .bvpropugt n),
+                (fun n => .app (.const ``BitVec.propsgt []) (.lit (.natVal n)), fun n => .bvpropsgt n)])
   ]
 
 /--
diff --git a/README.md b/README.md
index 684dff5..d3bd594 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,7 @@
 Type **"auto 👍"** to see whether auto is set up.
 
 ## Introduction
-Lean-auto is an interface between Lean and automated theorem provers, based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handeled by duper, a higher-order superposition prover written in Lean.  
+Lean-auto is an interface between Lean and automated theorem provers, based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handled by [Duper](https://github.com/leanprover-community/duper), a higher-order superposition prover written in Lean.  
 Lean-auto is still under development, but it's already able to solve nontrivial problems. For example the first part of the "snake lemma" in category theory can be solved by a direct invocation to ``auto`` (and the second part can also be partly automated):
 
 <img src="Doc/pics/shortfive.png" alt="drawing" width="500"/>
@@ -70,4 +70,4 @@ Lean-auto is still under development, but it's already able to solve nontrivial
 
 ## Checker
 * The checker is based on a deep embedding of simply-typed lambda calculus into dependent type theory.
-* The checker is slow on large input. For example, it takes ```6s``` to typecheck the final example in ```BinderComplexity.lean```. However, this is probably acceptable for mathlib usages, because e.g ```Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean``` has two theorems that take ```4s``` to compile (but a large portion of the ```4s``` are spent on typeclass inference)
\ No newline at end of file
+* The checker is slow on large input. For example, it takes ```6s``` to typecheck the final example in ```BinderComplexity.lean```. However, this is probably acceptable for mathlib usages, because e.g ```Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean``` has two theorems that take ```4s``` to compile (but a large portion of the ```4s``` are spent on typeclass inference)
diff --git a/Test/SmtTranslation/BitVec.lean b/Test/SmtTranslation/BitVec.lean
index 8d6e0fd..0e8039a 100644
--- a/Test/SmtTranslation/BitVec.lean
+++ b/Test/SmtTranslation/BitVec.lean
@@ -97,3 +97,13 @@ example
   (h2 : Std.BitVec.ult 0#64 j) :
   Std.BitVec.ult (max - (i + j)) (max - i) := by
   auto
+
+example : (2#6) < (3#6) := by auto
+
+example (a b : Std.BitVec 6) :
+  (a < b) = (a.ult b) ∧ (a ≤ b) = (a.ule b) := by auto
+
+theorem auto_bitvec_inequality_test (i j max : Std.BitVec 64)
+  (h0 : i < max) (h1 : j <= max - i) (h2 : 0#64 < j) :
+  (max - (i + j)) < (max - i) := by
+  auto
diff --git a/lake-manifest.json b/lake-manifest.json
index 9410f55..7e83f08 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "rev": "3959bc5de5142d06d7673ec091d406e5abe45bf0",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "auto",
diff --git a/lakefile.lean b/lakefile.lean
index d4c2188..2dea24a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,11 +2,12 @@ import Lake
 open Lake DSL
 
 package «auto» {
-  -- add any package configuration options here
+  precompileModules := true
+  preferReleaseBuild := true
 }
 
 require std from git
-  "https://github.com/leanprover/std4.git"@"9e37a01f8590f81ace095b56710db694b5bf8ca0"
+  "https://github.com/leanprover/std4.git"@"main"
 
 @[default_target]
 lean_lib «Auto» {
diff --git a/lean-toolchain b/lean-toolchain
index 91ccf6a..0927c52 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:v4.5.0-rc1
\ No newline at end of file