diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index 969171950e..aad6587644 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -75,9 +75,7 @@ instance : ToExpr Gate where
   toExpr x :=
     match x with
     | .and => mkConst ``Gate.and
-    | .or => mkConst ``Gate.or
     | .xor => mkConst ``Gate.xor
-    | .imp => mkConst ``Gate.imp
     | .beq => mkConst ``Gate.beq
   toTypeExpr := mkConst ``Gate
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
index 0a1e800582..4a80fb3e09 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
@@ -65,7 +65,6 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
       let subProof ← sub.evalsAtAtoms
       return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
     return some ⟨boolExpr, proof, expr⟩
-  | Bool.or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
   | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
   | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
   | BEq.beq α _ lhsExpr rhsExpr =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
index 4f0390e9a8..8797391eba 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
@@ -16,26 +16,20 @@ namespace Std.Tactic.BVDecide
 
 inductive Gate
   | and
-  | or
   | xor
   | beq
-  | imp
 
 namespace Gate
 
 def toString : Gate → String
   | and => "&&"
-  | or  => "||"
   | xor => "^^"
   | beq => "=="
-  | imp => "→"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
-  | or => (· || ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
-  | imp => (!· || ·)
 
 end Gate
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
index 8641684e5e..b2143d6544 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
@@ -51,10 +51,6 @@ where
         let ret := aig.mkAndCached input
         have := LawfulOperator.le_size (f := mkAndCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .or =>
-        let ret := aig.mkOrCached input
-        have := LawfulOperator.le_size (f := mkOrCached) aig input
-        ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
       | .xor =>
         let ret := aig.mkXorCached input
         have := LawfulOperator.le_size (f := mkXorCached) aig input
@@ -63,11 +59,6 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .imp =>
-        let ret := aig.mkImpCached input
-        have := LawfulOperator.le_size (f := mkImpCached) aig input
-        ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-
 
 variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]
 
@@ -99,18 +90,12 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
     | and =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
-    | or =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
     | xor =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
-    | imp =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
 
 theorem ofBoolExprCached.go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index f4719c50a8..11662260a2 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -121,10 +121,6 @@ theorem and_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' && rhs') = (lhs && rhs) := by
   simp[*]
 
-theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (lhs' || rhs') = (lhs || rhs) := by
-  simp[*]
-
 theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
     (lhs' ^^ rhs') = (lhs ^^ rhs) := by
   simp[*]
diff --git a/tests/lean/run/aig_shared.lean b/tests/lean/run/aig_shared.lean
index 0a7d8304d3..0aa1b129b2 100644
--- a/tests/lean/run/aig_shared.lean
+++ b/tests/lean/run/aig_shared.lean
@@ -8,44 +8,41 @@ def mkSharedTree (n : Nat) : BoolExpr Nat :=
   | 0 => .literal 0
   | n + 1 =>
     let tree := mkSharedTree n
-    .gate .or tree tree
+    .gate .xor tree tree
 
 /--
-info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
-  Std.Sat.AIG.Decl.gate 1 2 true false]
+info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true]
 -/
 #guard_msgs in
 #eval ofBoolExprCached (mkSharedTree 1) AIG.mkAtomCached |>.aig.decls
 
 /--
-info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
-  Std.Sat.AIG.Decl.gate 1 2 true false, Std.Sat.AIG.Decl.gate 3 3 true true, Std.Sat.AIG.Decl.gate 2 4 false true]
+info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
+  Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true]
 -/
 #guard_msgs in
 #eval ofBoolExprCached (mkSharedTree 2) AIG.mkAtomCached |>.aig.decls
 
 /--
-info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
-  Std.Sat.AIG.Decl.gate 1 2 true false, Std.Sat.AIG.Decl.gate 3 3 true true, Std.Sat.AIG.Decl.gate 2 4 false true,
-  Std.Sat.AIG.Decl.gate 5 5 true true, Std.Sat.AIG.Decl.gate 2 6 false true, Std.Sat.AIG.Decl.gate 7 7 true true,
-  Std.Sat.AIG.Decl.gate 2 8 false true]
+info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
+  Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true,
+  Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true]
 -/
 #guard_msgs in
 #eval ofBoolExprCached (mkSharedTree 4) AIG.mkAtomCached |>.aig.decls
 
 /--
-info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.const true,
-  Std.Sat.AIG.Decl.gate 1 2 true false, Std.Sat.AIG.Decl.gate 3 3 true true, Std.Sat.AIG.Decl.gate 2 4 false true,
-  Std.Sat.AIG.Decl.gate 5 5 true true, Std.Sat.AIG.Decl.gate 2 6 false true, Std.Sat.AIG.Decl.gate 7 7 true true,
-  Std.Sat.AIG.Decl.gate 2 8 false true, Std.Sat.AIG.Decl.gate 9 9 true true, Std.Sat.AIG.Decl.gate 2 10 false true,
-  Std.Sat.AIG.Decl.gate 11 11 true true, Std.Sat.AIG.Decl.gate 2 12 false true, Std.Sat.AIG.Decl.gate 13 13 true true,
-  Std.Sat.AIG.Decl.gate 2 14 false true, Std.Sat.AIG.Decl.gate 15 15 true true, Std.Sat.AIG.Decl.gate 2 16 false true,
-  Std.Sat.AIG.Decl.gate 17 17 true true, Std.Sat.AIG.Decl.gate 2 18 false true, Std.Sat.AIG.Decl.gate 19 19 true true,
-  Std.Sat.AIG.Decl.gate 2 20 false true, Std.Sat.AIG.Decl.gate 21 21 true true, Std.Sat.AIG.Decl.gate 2 22 false true,
-  Std.Sat.AIG.Decl.gate 23 23 true true, Std.Sat.AIG.Decl.gate 2 24 false true, Std.Sat.AIG.Decl.gate 25 25 true true,
-  Std.Sat.AIG.Decl.gate 2 26 false true, Std.Sat.AIG.Decl.gate 27 27 true true, Std.Sat.AIG.Decl.gate 2 28 false true,
-  Std.Sat.AIG.Decl.gate 29 29 true true, Std.Sat.AIG.Decl.gate 2 30 false true, Std.Sat.AIG.Decl.gate 31 31 true true,
-  Std.Sat.AIG.Decl.gate 2 32 false true]
+info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
+  Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true,
+  Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true,
+  Std.Sat.AIG.Decl.gate 8 8 true true, Std.Sat.AIG.Decl.gate 8 9 true true, Std.Sat.AIG.Decl.gate 10 10 true true,
+  Std.Sat.AIG.Decl.gate 10 11 true true, Std.Sat.AIG.Decl.gate 12 12 true true, Std.Sat.AIG.Decl.gate 12 13 true true,
+  Std.Sat.AIG.Decl.gate 14 14 true true, Std.Sat.AIG.Decl.gate 14 15 true true, Std.Sat.AIG.Decl.gate 16 16 true true,
+  Std.Sat.AIG.Decl.gate 16 17 true true, Std.Sat.AIG.Decl.gate 18 18 true true, Std.Sat.AIG.Decl.gate 18 19 true true,
+  Std.Sat.AIG.Decl.gate 20 20 true true, Std.Sat.AIG.Decl.gate 20 21 true true, Std.Sat.AIG.Decl.gate 22 22 true true,
+  Std.Sat.AIG.Decl.gate 22 23 true true, Std.Sat.AIG.Decl.gate 24 24 true true, Std.Sat.AIG.Decl.gate 24 25 true true,
+  Std.Sat.AIG.Decl.gate 26 26 true true, Std.Sat.AIG.Decl.gate 26 27 true true, Std.Sat.AIG.Decl.gate 28 28 true true,
+  Std.Sat.AIG.Decl.gate 28 29 true true, Std.Sat.AIG.Decl.gate 30 30 true true, Std.Sat.AIG.Decl.gate 30 31 true true]
 -/
 #guard_msgs in
 #eval ofBoolExprCached (mkSharedTree 16) AIG.mkAtomCached |>.aig.decls