diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean
index df6c1498..0c1dc251 100644
--- a/Smt/Reconstruct/Int.lean
+++ b/Smt/Reconstruct/Int.lean
@@ -95,15 +95,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_PLUS_ZERO =>
     if !pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_zero) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_zero) args)
   | .ARITH_MUL_ONE =>
     if !pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_one) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mul_one) args)
   | .ARITH_MUL_ZERO =>
     if !pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_zero) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mul_zero) args)
   | .ARITH_INT_DIV_TOTAL =>
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
     let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
@@ -199,23 +199,23 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_PLUS_FLATTEN =>
     if !pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_flatten) args)
   | .ARITH_MULT_FLATTEN =>
     if !pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mult_flatten) args)
   | .ARITH_MULT_DIST =>
     if !pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_dist) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mult_dist) args)
   | .ARITH_PLUS_CANCEL1 =>
     if !pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.plus_cancel1) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_cancel1) args)
   | .ARITH_PLUS_CANCEL2 =>
     if !pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_cancel2) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_cancel2) args)
   | .ARITH_ABS_ELIM =>
     if !pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
@@ -226,8 +226,11 @@ where
     let mut args' := #[]
     for arg in args do
       let mut arg' := #[]
-      for subarg in arg do
-        arg' := arg'.push (← reconstructTerm subarg)
+      if arg.getKind == .SEXPR then
+        for subarg in arg do
+          arg' := arg'.push (← reconstructTerm subarg)
+      else
+        arg' := arg'.push (← reconstructTerm arg)
       args' := args'.push arg'
     return args'
 
diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean
index 7845d6b7..7a3502cb 100644
--- a/Smt/Reconstruct/Prop.lean
+++ b/Smt/Reconstruct/Prop.lean
@@ -80,46 +80,46 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     addThm q(($p → $q) = (¬$p ∨ $q)) q(@Prop.bool_impl_elim $p $q)
-  -- | .BOOL_OR_TRUE =>
-  --   let args ← reconstructArgs pf.getArguments
-  --   addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_true) args)
+  | .BOOL_OR_TRUE =>
+    let args ← reconstructArgs pf.getArguments
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_true) args)
   | .BOOL_OR_FALSE =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_false) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_false) args)
   | .BOOL_OR_FLATTEN =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_flatten) args)
   | .BOOL_OR_DUP =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_dup) args)
-  -- | .BOOL_AND_TRUE =>
-  --   let args ← reconstructArgs pf.getArguments[1:]
-  --   addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_true) args)
-  -- | .BOOL_AND_FALSE =>
-  --   let args ← reconstructArgs pf.getArguments[1:]
-  --   addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_false) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_dup) args)
+  | .BOOL_AND_TRUE =>
+    let args ← reconstructArgs pf.getArguments[1:]
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_true) args)
+  | .BOOL_AND_FALSE =>
+    let args ← reconstructArgs pf.getArguments[1:]
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_false) args)
   | .BOOL_AND_FLATTEN =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_flatten) args)
   | .BOOL_AND_DUP =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_dup) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_dup) args)
   | .BOOL_AND_CONF =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_conf) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_conf) args)
   | .BOOL_OR_TAUT =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_taut) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_taut) args)
   | .BOOL_OR_DE_MORGAN =>
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_de_morgan) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_de_morgan) args)
   | .BOOL_IMPLIES_DE_MORGAN =>
     let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     addThm q((¬($p → $q)) = ($p ∧ ¬$q)) q(@Prop.bool_implies_de_morgan $p $q)
-  -- | .BOOL_AND_DE_MORGAN =>
-  --   let args ← reconstructArgs pf.getArguments[1:]
-  --   addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_de_morgan) args)
+  | .BOOL_AND_DE_MORGAN =>
+    let args ← reconstructArgs pf.getArguments[1:]
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_de_morgan) args)
   | .BOOL_XOR_REFL =>
     let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p)
@@ -191,8 +191,11 @@ where
     let mut args' := #[]
     for arg in args do
       let mut arg' := #[]
-      for subarg in arg do
-        arg' := arg'.push (← reconstructTerm subarg)
+      if arg.getKind == .SEXPR then
+        for subarg in arg do
+          arg' := arg'.push (← reconstructTerm subarg)
+      else
+        arg' := arg'.push (← reconstructTerm arg)
       args' := args'.push arg'
     return args'
 
diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean
index acdd332b..9be8dab6 100644
--- a/Smt/Reconstruct/Rat.lean
+++ b/Smt/Reconstruct/Rat.lean
@@ -110,15 +110,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_PLUS_ZERO =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_zero) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_zero) args)
   | .ARITH_MUL_ONE =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_one) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mul_one) args)
   | .ARITH_MUL_ZERO =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_zero) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mul_zero) args)
   | .ARITH_DIV_TOTAL =>
     let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
     let s : Q(Rat) ← reconstructTerm pf.getArguments[2]!
@@ -181,23 +181,23 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_PLUS_FLATTEN =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_flatten) args)
   | .ARITH_MULT_FLATTEN =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mult_flatten) args)
   | .ARITH_MULT_DIST =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_dist) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mult_dist) args)
   | .ARITH_PLUS_CANCEL1 =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.plus_cancel1) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_cancel1) args)
   | .ARITH_PLUS_CANCEL2 =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_cancel2) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_cancel2) args)
   | .ARITH_ABS_ELIM =>
     if pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
@@ -208,8 +208,11 @@ where
     let mut args' := #[]
     for arg in args do
       let mut arg' := #[]
-      for subarg in arg do
-        arg' := arg'.push (← reconstructTerm subarg)
+      if arg.getKind == .SEXPR then
+        for subarg in arg do
+          arg' := arg'.push (← reconstructTerm subarg)
+      else
+        arg' := arg'.push (← reconstructTerm arg)
       args' := args'.push arg'
     return args'
 
diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean
index 22858d22..6675918b 100644
--- a/Smt/Reconstruct/Real.lean
+++ b/Smt/Reconstruct/Real.lean
@@ -130,15 +130,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_PLUS_ZERO =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_zero) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_zero) args)
   | .ARITH_MUL_ONE =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mul_one) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mul_one) args)
   | .ARITH_MUL_ZERO =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mul_zero) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mul_zero) args)
   | .ARITH_DIV_TOTAL =>
     let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
     let s : Q(Real) ← reconstructTerm pf.getArguments[2]!
@@ -201,23 +201,23 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_PLUS_FLATTEN =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_flatten) args)
   | .ARITH_MULT_FLATTEN =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mult_flatten) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mult_flatten) args)
   | .ARITH_MULT_DIST =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mult_dist) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mult_dist) args)
   | .ARITH_PLUS_CANCEL1 =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.plus_cancel1) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_cancel1) args)
   | .ARITH_PLUS_CANCEL2 =>
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_cancel2) args)
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_cancel2) args)
   | .ARITH_ABS_ELIM =>
     if pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
@@ -228,8 +228,11 @@ where
     let mut args' := #[]
     for arg in args do
       let mut arg' := #[]
-      for subarg in arg do
-        arg' := arg'.push (← reconstructTerm subarg)
+      if arg.getKind == .SEXPR then
+        for subarg in arg do
+          arg' := arg'.push (← reconstructTerm subarg)
+      else
+        arg' := arg'.push (← reconstructTerm arg)
       args' := args'.push arg'
     return args'
 
diff --git a/Smt/Reconstruct/Rewrite.lean b/Smt/Reconstruct/Rewrite.lean
index 36a7b2da..ec5f3f07 100644
--- a/Smt/Reconstruct/Rewrite.lean
+++ b/Smt/Reconstruct/Rewrite.lean
@@ -9,6 +9,9 @@ import Lean
 
 import Smt.Reconstruct.Prop.Rewrites
 
+theorem Eq.trans₂ {α} {a b c d : α} (h₁ : a = b) (h₂ : b = c) (h₃ : c = d) : a = d :=
+  h₁ ▸ h₂ ▸ h₃
+
 namespace Smt.Reconstruct.Tactic
 
 open Lean Elab.Tactic
@@ -19,26 +22,20 @@ def traceSmtRw (r : Except Exception Unit) : MetaM MessageData :=
   | .ok _ => m!"{checkEmoji}"
   | _     => m!"{bombEmoji}"
 
-def smtRw (mv : MVarId) (assoc : Expr) (null : Expr) (rule : Expr) (arr : Array (Array Expr)) : MetaM Unit :=
+def smtRw (mv : MVarId) (op : Expr) (id : Expr) (rr : Expr) (xss : Array (Array Expr)) : MetaM Unit :=
   withTraceNode `smt.reconstruct.smtRw traceSmtRw do
-  let n := arr.size
-  let mut mv' := mv
-  for i in [: n] do
-    let m := arr[i]!.size
-    if m > 1 then
-      for j in [: m-1] do
-        if let some r ← observing? (mv'.rewrite (← mv'.getType) (mkAppN assoc #[arr[i]![m-j-2]!]) true) then
-          mv' ← mv'.replaceTargetEq r.eNew r.eqProof
-  if let some r ← observing? (mv'.rewrite (← mv'.getType) rule) then
-    mv' ← mv'.replaceTargetEq r.eNew r.eqProof
-  if let some r ← observing? (mv'.rewrite (← mv'.getType) null) then
-    mv' ← mv'.replaceTargetEq r.eNew r.eqProof
-  for i in [: n] do
-    let m := arr[i]!.size
-    for j in [: m-1] do
-      if let some r ← observing? (mv'.rewrite (← mv'.getType) (.app assoc arr[i]![j]!)) then
-        mv' ← mv'.replaceTargetEq r.eNew r.eqProof
-  mv'.refl
+  let xs := xss.map (fun xs => xs[1:].foldr (mkApp2 op) (xs[0]?.getD id))
+  let some (α, l, r) := (← mv.getType).eq?
+    | throwError "[smt_rw] expected a top level equality with AC operator on lhs and/or rhs, got {← mv.getType}"
+  let h₂ := mkAppN rr xs
+  let some (_, ml, mr) := (← Meta.inferType h₂).eq?
+    | throwError "[smt_rw] error applying rewrite rule to arguments: {mkAppN rr xs}"
+  let lvl ← Meta.getLevel α
+  let h₁ ← Meta.mkFreshExprMVar (mkApp3 (.const ``Eq [lvl]) α l ml)
+  let h₃ ← Meta.mkFreshExprMVar (mkApp3 (.const ``Eq [lvl]) α mr r)
+  Meta.AC.rewriteUnnormalized h₁.mvarId!
+  Meta.AC.rewriteUnnormalized h₃.mvarId!
+  mv.assign (mkApp8 (.const ``Eq.trans₂ [lvl]) α l ml mr r h₁ h₂ h₃)
 
 syntax inner := "[" term,* "]"
 syntax outer := "[" inner,* "]"
@@ -54,29 +51,32 @@ def parseOuter : TSyntax ``outer → TacticM (Array (Array Expr))
   | _ => throwError "[outer]: wrong usage"
 
 @[tactic smt_rw] def evalSMTRw : Tactic := fun stx => do
-  let mv : MVarId ← getMainGoal
-  let rr ← elabTerm stx[3] none
+  let op ← elabTermForApply stx[1]
+  let id ← elabTermForApply stx[2]
+  let rr ← elabTermForApply stx[3]
   let xs ← parseOuter ⟨stx[4]⟩
-  let op  ← elabTermForApply stx[1]
-  let nu  ← elabTermForApply stx[2]
-  smtRw mv op nu rr xs
+  let mv : MVarId ← getMainGoal
+  smtRw mv op id rr xs
 
 example : (x1 ∧ x2 ∧ x3 ∧ (b ∧ y1 ∧ y2 ∧ True) ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by
-  smt_rw and_assoc_eq and_true bool_and_flatten [[x1, x2], [b], [y1, y2], [z1, z2]]
+  smt_rw And True bool_and_flatten [[x1, x2, x3], [b], [y1, y2], [z1, z2]]
 
 example : (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ b ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by
-  smt_rw and_assoc_eq and_true bool_and_dup [[x1, x2, x3], [b], [y1, y2], [b], [z1, z2]]
+  smt_rw And True bool_and_flatten [[x1, x2, x3], [b], [y1, y2], [z1, z2]]
 
 example : (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ y2 ∨ b ∨ z1 ∨ z2 ∨ False) = (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ y2 ∨ z1 ∨ z2 ∨ False) := by
-  smt_rw or_assoc_eq or_false bool_or_dup [[x1, x2, x3], [b], [y1, y2], [b], [z1, z2]]
+  smt_rw Or False bool_or_flatten [[x1, x2, x3], [b], [y1, y2], [z1, z2]]
 
 example : (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ b ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by
-  smt_rw and_assoc_eq and_true bool_and_dup [[x1, x2, x3], [b], [y1, y2], [b], [z1, z2]]
+  smt_rw And True bool_and_dup [[x1, x2, x3], [b], [y1, y2], [z1, z2]]
 
 example : (x1 ∨ x2 ∨ x3 ∨ (b ∨  y1 ∨ False) ∨ z1 ∨ False) = (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ z1 ∨ False) := by
-  smt_rw or_assoc_eq or_false bool_or_flatten [[x1, x2, x3], [b], [y1], [z1]]
+  smt_rw Or False bool_or_flatten [[x1, x2, x3], [b], [y1], [z1]]
 
 example : (p1 ∧ True) = p1 := by
-  smt_rw and_assoc_eq and_true bool_and_true [[p1], []]
+  smt_rw And True bool_and_true [[p1], []]
+
+example : (p ∨ ¬p) = True := by
+  smt_rw Or False bool_or_taut [[], [p], [], []]
 
 end Smt.Reconstruct.Tactic
diff --git a/Test/EUF/Issue126.expected b/Test/EUF/Issue126.expected
index f2579f65..e69de29b 100644
--- a/Test/EUF/Issue126.expected
+++ b/Test/EUF/Issue126.expected
@@ -1 +0,0 @@
-Test/EUF/Issue126.lean:3:8: warning: declaration uses 'sorry'
diff --git a/Test/EUF/Issue126.lean b/Test/EUF/Issue126.lean
index f8e68926..3e474bae 100644
--- a/Test/EUF/Issue126.lean
+++ b/Test/EUF/Issue126.lean
@@ -78,4 +78,3 @@ theorem extracted_1 (n a r v : Type)
         ∃ q,
           ngt q ∧ ∀ (s : a), nmm s q → tc s n o r v := by
   smt [nsih, noh, nsg, nne, ha, hb]
-  all_goals sorry
diff --git a/Test/Prop/Triv'.expected b/Test/Prop/Triv'.expected
index 0439c450..e69de29b 100644
--- a/Test/Prop/Triv'.expected
+++ b/Test/Prop/Triv'.expected
@@ -1,8 +0,0 @@
-Test/Prop/Triv'.lean:4:2: error: tactic 'rfl' failed, equality lhs
-  p ∨ ¬p
-is not definitionally equal to rhs
-  True
-case s.2
-a.0 : ¬∀ (p : Prop), p → p
-p : Prop
-⊢ (p ∨ ¬p) = True
diff --git a/Test/Prop/Triv'.lean b/Test/Prop/Triv'.lean
index 0f435c42..cd9a1d52 100644
--- a/Test/Prop/Triv'.lean
+++ b/Test/Prop/Triv'.lean
@@ -2,7 +2,3 @@ import Smt
 
 example : ∀ p : Prop, p → p := by
   smt
-  all_goals
-    intros; apply propext; apply Iff.intro
-    · intros; trivial
-    · intros; simp_all