diff --git a/Smt.lean b/Smt.lean
index f82fe5f7..01883050 100644
--- a/Smt.lean
+++ b/Smt.lean
@@ -5,6 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct
+import Smt.Arith
+import Smt.BitVec
+import Smt.Bool
+import Smt.Builtin
+import Smt.Nat
+import Smt.Prop
+import Smt.Quant
+import Smt.String
 import Smt.Tactic
-import Smt.Translate
+import Smt.UF
diff --git a/Smt/Arith.lean b/Smt/Arith.lean
new file mode 100644
index 00000000..7d3dd8df
--- /dev/null
+++ b/Smt/Arith.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomaz Gomes Mascarenhas
+-/
+
+import Smt.Reconstruct.Arith
+import Smt.Translate.Int
+import Smt.Translate.Real
diff --git a/Smt/BitVec.lean b/Smt/BitVec.lean
new file mode 100644
index 00000000..47fdc2b4
--- /dev/null
+++ b/Smt/BitVec.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Reconstruct.BitVec
+import Smt.Translate.BitVec
diff --git a/Smt/Bool.lean b/Smt/Bool.lean
new file mode 100644
index 00000000..800ec8ad
--- /dev/null
+++ b/Smt/Bool.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Translate.Bool
diff --git a/Smt/Builtin.lean b/Smt/Builtin.lean
new file mode 100644
index 00000000..4177b8aa
--- /dev/null
+++ b/Smt/Builtin.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Reconstruct.Builtin
diff --git a/Smt/Nat.lean b/Smt/Nat.lean
new file mode 100644
index 00000000..c4368305
--- /dev/null
+++ b/Smt/Nat.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Translate.Nat
diff --git a/Smt/Prop.lean b/Smt/Prop.lean
new file mode 100644
index 00000000..51e24ad8
--- /dev/null
+++ b/Smt/Prop.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Reconstruct.Prop
+import Smt.Translate.Prop
diff --git a/Smt/Quant.lean b/Smt/Quant.lean
new file mode 100644
index 00000000..99a67d1e
--- /dev/null
+++ b/Smt/Quant.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Reconstruct.Quant
diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean
index b746d724..b3f9afe4 100644
--- a/Smt/Reconstruct.lean
+++ b/Smt/Reconstruct.lean
@@ -5,10 +5,220 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.Arith
-import Smt.Reconstruct.BitVec
-import Smt.Reconstruct.Builtin
-import Smt.Reconstruct.Options
-import Smt.Reconstruct.Prop
-import Smt.Reconstruct.Quant
-import Smt.Reconstruct.UF
+import cvc5
+import Qq
+import Std
+
+import Smt.Attribute
+
+namespace Smt
+
+open Lean
+open Attribute
+
+structure Reconstruct.state where
+  termCache : HashMap cvc5.Term Expr
+  proofCache : HashMap cvc5.Proof Expr
+  count : Nat
+  trusts : Array cvc5.Proof
+  mainGoal : MVarId
+  currGoal : MVarId
+  currAssums : Array Expr
+  skipedGoals : Array MVarId
+
+abbrev ReconstructM := StateT Reconstruct.state MetaM
+
+abbrev SortReconstructor := cvc5.Sort → ReconstructM (Option Expr)
+
+abbrev TermReconstructor := cvc5.Term → ReconstructM (Option Expr)
+
+abbrev ProofReconstructor := cvc5.Proof → ReconstructM (Option Expr)
+
+namespace Reconstruct
+
+private unsafe def getReconstructorsUnsafe (n : Name) (rcons : Type) : MetaM (List (rcons × Name)) := do
+  let env ← getEnv
+  let names := ((smtExt.getState env).findD n {}).toList
+  let mut reconstructors := []
+  for name in names do
+    let fn ← IO.ofExcept <| Id.run <| ExceptT.run <|
+      env.evalConst rcons Options.empty name
+    reconstructors := (fn, name) :: reconstructors
+  return reconstructors
+
+@[implemented_by getReconstructorsUnsafe]
+opaque getReconstructors (n : Name) (rcons : Type) : MetaM (List (rcons × Name))
+
+def reconstructSort (s : cvc5.Sort) : ReconstructM Expr := do
+  let rs ← getReconstructors ``SortReconstructor SortReconstructor
+  go rs s
+where
+  go (rs : List (SortReconstructor × Name)) (s : cvc5.Sort) : ReconstructM Expr := do
+    for (r, n) in rs do
+      if let some e ← r s then
+        trace[smt.debug.reconstruct.sort] "{s} =({n})=> {e}"
+        return e
+    throwError "Failed to reconstruct sort {s} with kind {repr s.getKind}"
+
+def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : ReconstructM MessageData :=
+  return m!"{t} ↦ " ++ match r with
+    | .ok e    => m!"{e}"
+    | .error _ => m!"{bombEmoji}"
+
+def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t =>
+  withTraceNode `smt.debug.reconstruct (traceReconstructTerm t) do
+    let rs ← getReconstructors ``TermReconstructor TermReconstructor
+    go rs t
+where
+  withTermCache (r : cvc5.Term → ReconstructM Expr) (t : cvc5.Term) : ReconstructM Expr := do
+    match (← get).termCache.find? t with
+    -- TODO: cvc5's global bound variables mess up the cache. Find a fix.
+    | some e => if e.hasFVar then reconstruct r t else return e
+    | none   => reconstruct r t
+  reconstruct r t := do
+    let e ← r t
+    modify fun state => { state with termCache := state.termCache.insert t e }
+    return e
+  go (rs : List (TermReconstructor × Name)) (t : cvc5.Term) : ReconstructM Expr := do
+    for (r, n) in rs do
+      if let some e ← r t then
+        trace[smt.debug.reconstruct.term] "{t} =({n})=> {e}"
+        return e
+    throwError "Failed to reconstruct term {t} with kind {repr t.getKind}"
+
+def withProofCache (r : cvc5.Proof → ReconstructM Expr) (p : cvc5.Proof) : ReconstructM Expr := do
+  match (← get).proofCache.find? p with
+  | some e => (← get).currGoal.withContext do
+    if (← getLCtx).containsFVar e then return e else reconstruct r p
+  | none   => reconstruct r p
+where
+  reconstruct r p := do
+    let e ← r p
+    modify fun state => { state with proofCache := state.proofCache.insert p e }
+    return e
+
+def incCount : ReconstructM Nat :=
+  modifyGet fun state => (state.count, { state with count := state.count + 1 })
+
+def withAssums (as : Array Expr) (k : ReconstructM α) : ReconstructM α := do
+  modify fun state => { state with currAssums := state.currAssums ++ as }
+  let r ← k
+  modify fun state => { state with currAssums := state.currAssums.shrink (state.currAssums.size - as.size) }
+  return r
+
+def skipStep (mv : MVarId) : ReconstructM Unit := mv.withContext do
+  let state ← get
+  let t ← Meta.mkForallFVars state.currAssums (← mv.getType)
+  let mv' ← state.mainGoal.withContext (Meta.mkFreshExprMVar t)
+  let e := mkAppN mv' state.currAssums
+  set { state with skipedGoals := state.skipedGoals.push mv'.mvarId! }
+  mv.assignIfDefeq e
+
+def getCurrGoal : ReconstructM MVarId :=
+  get >>= (pure ·.currGoal)
+
+def setCurrGoal (mv : MVarId) : ReconstructM Unit :=
+  modify fun state => { state with currGoal := mv }
+
+def addThm (type : Expr) (val : Expr) : ReconstructM Expr := do
+  let mv ← getCurrGoal
+  mv.withContext do
+    let name := Name.num `s (← incCount)
+    let (fv, mv) ← (← mv.assert name type val).intro1P
+    trace[smt.debug.reconstruct.proof] "have {name} : {type} := {val}"
+    setCurrGoal mv
+    return .fvar fv
+
+def addTac (type : Expr) (tac : MVarId → MetaM Unit) : ReconstructM Expr := do
+  let mv ← getCurrGoal
+  mv.withContext do
+    let name := Name.num `s (← incCount)
+    let mv' ← Meta.mkFreshExprMVar type
+    tac mv'.mvarId!
+    let (fv, mv) ← (← mv.assert name type mv').intro1P
+    trace[smt.debug.reconstruct.proof] "have {name} : {type} := by {mv'}"
+    setCurrGoal mv
+    return .fvar fv
+
+def addTrust (type : Expr) (pf : cvc5.Proof) : ReconstructM Expr := do
+  let mv ← getCurrGoal
+  mv.withContext do
+    let name := Name.num `s (← incCount)
+    let mv' ← Meta.mkFreshExprMVar type
+    skipStep mv'.mvarId!
+    let (fv, mv) ← (← mv.assert name type mv').intro1P
+    trace[smt.debug.reconstruct.proof] m!"have {name} : {type} := sorry"
+    trace[smt.debug.reconstruct.proof]
+      m!"rule : {repr pf.getRule}\npremises : {pf.getChildren.map (·.getResult)}\nargs : {pf.getArguments}\nconclusion : {pf.getResult}"
+    modify fun state => { state with trusts := state.trusts.push pf }
+    setCurrGoal mv
+    return .fvar fv
+
+partial def reconstructProof : cvc5.Proof → ReconstructM Expr := withProofCache fun pf => do
+  let rs ← getReconstructors ``ProofReconstructor ProofReconstructor
+  go rs pf
+where
+  go (rs : List (ProofReconstructor × Name)) (pf : cvc5.Proof) : ReconstructM Expr := do
+    for (r, _) in rs do
+      if let some e ← r pf then
+        return e
+    _ ← pf.getChildren.mapM reconstructProof
+    let type ← reconstructTerm pf.getResult
+    addTrust type pf
+
+end Reconstruct
+
+def traceReconstructProof (r : Except Exception (FVarId × MVarId × List MVarId)) : MetaM MessageData :=
+  return match r with
+  | .ok _ => m!"{checkEmoji}"
+  | _     => m!"{bombEmoji}"
+
+open Qq in
+partial def reconstructProof (mv : MVarId) (pf : cvc5.Proof) : MetaM (FVarId × MVarId × List MVarId) :=
+  withTraceNode `smt.debug.reconstruct traceReconstructProof do
+  let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨{}, {}, 0, #[], mv, mv, #[], #[]⟩
+  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mv _ mvs) ← (Reconstruct.reconstructProof pf).run state
+  let ⟨fv, mv, _⟩ ← mv.replace h.fvarId! q($h trivial) q($p)
+  return (fv, mv, mvs.toList)
+
+open cvc5 in
+def traceProve (r : Except Exception (Except SolverError Proof)) : MetaM MessageData :=
+  return match r with
+  | .ok (.ok _) => m!"{checkEmoji}"
+  | _           => m!"{bombEmoji}"
+
+open cvc5 in
+def prove (query : String) (timeout : Option Nat) : MetaM (Except SolverError cvc5.Proof) :=
+  withTraceNode `smt.debug.prove traceProve do Solver.run do
+    if let .some timeout := timeout then
+      Solver.setOption "tlimit" (toString (1000*timeout))
+    Solver.setOption "dag-thresh" "0"
+    Solver.setOption "simplification" "none"
+    Solver.setOption "enum-inst" "true"
+    Solver.setOption "produce-models" "true"
+    Solver.setOption "produce-proofs" "true"
+    Solver.setOption "proof-elim-subtypes" "true"
+    Solver.setOption "proof-granularity" "dsl-rewrite"
+    Solver.parse query
+    let r ← Solver.checkSat
+    if r.isUnsat then
+      let ps ← Solver.getProof
+      if h : 0 < ps.size then
+        trace[smt.debug.reconstruct] (← Solver.proofToString ps[0])
+        return ps[0]
+    throw (self := instMonadExcept _ _) (SolverError.user_error "something went wrong")
+
+syntax (name := reconstruct) "reconstruct" str : tactic
+
+open Lean.Elab Tactic in
+@[tactic reconstruct] def evalReconstruct : Tactic := fun stx =>
+  withMainContext do
+    let some query := stx[1].isStrLit? | throwError "expected string"
+    let r ← prove query none
+    match r with
+      | .error e => logInfo (repr e)
+      | .ok pf =>
+        let (_, mv, mvs) ← reconstructProof (← getMainGoal) pf
+        replaceMainGoal (mv :: mvs)
+
+end Smt
diff --git a/Smt/Reconstruct/Arith.lean b/Smt/Reconstruct/Arith.lean
index f1c507ba..2448ce3b 100644
--- a/Smt/Reconstruct/Arith.lean
+++ b/Smt/Reconstruct/Arith.lean
@@ -2,7 +2,139 @@
 Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
 institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Tomaz Gomes Mascarenhas
+Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.Arith.Reconstruct
+import Smt.Reconstruct.Arith.ArithMulSign
+import Smt.Reconstruct.Arith.MulPosNeg
+import Smt.Reconstruct.Arith.Rewrites
+import Smt.Reconstruct.Arith.SumBounds
+import Smt.Reconstruct.Arith.Rewrites
+import Smt.Reconstruct.Arith.TangentPlane
+import Smt.Reconstruct.Arith.TightBounds
+import Smt.Reconstruct.Arith.Trichotomy
+import Smt.Reconstruct
+
+namespace Smt.Reconstruct.Arith
+
+open Lean hiding Rat
+open Qq
+
+@[smt_sort_reconstruct] def reconstructArithSort : SortReconstructor := fun s => do match s.getKind with
+  | .INTEGER_SORT => return q(Int)
+  | .REAL_SORT    => return q(Real)
+  | _             => return none
+
+def getTypeAndInst (s : cvc5.Sort) : Σ α : Q(Type), Q(LinearOrderedRing $α) := match s.isInteger with
+  | false => ⟨q(Real), q(Real.instLinearOrderedRingReal)⟩
+  | true  => ⟨q(Int), q(Int.linearOrderedCommRing.toLinearOrderedRing)⟩
+
+
+@[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
+  | .SKOLEM_FUN => match t.getSkolemId with
+    | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0)
+    | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0)
+    | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0)
+    | _ => return none
+  | .CONST_INTEGER =>
+    let x : Int := t.getIntegerValue
+    let x' : Q(Nat) := mkRawNatLit x.natAbs
+    if x ≥ 0 then
+      return q(OfNat.ofNat $x' : Int)
+    else
+      return q(-(OfNat.ofNat $x' : Int))
+  | .CONST_RATIONAL =>
+    let x : Rat := t.getRationalValue
+    let num : Q(Real) := mkRealLit x.num.natAbs
+    if x.den == 1 then
+      if x.num ≥ 0 then
+        return q($num)
+      else
+        return q(-$num)
+    else
+      let den : Q(Real) := mkRealLit x.den
+      if x.num ≥ 0 then
+        return q($num / $den)
+      else
+        return q(-$num / $den)
+  | .NEG =>
+    let ⟨α, _⟩ := getTypeAndInst t.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    return q(-$x)
+  | .SUB =>
+    let ⟨α, _⟩ := getTypeAndInst t.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x - $y)
+  | .ADD =>
+    let ⟨α, _⟩ := getTypeAndInst t.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x + $y)
+  | .MULT =>
+    let ⟨α, _⟩ := getTypeAndInst t.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x * $y)
+  | .INTS_DIVISION =>
+    let x : Q(Int) ← reconstructTerm t[0]!
+    let y : Q(Int) ← reconstructTerm t[1]!
+    return q($x / $y)
+  | .INTS_MODULUS =>
+    let x : Q(Int) ← reconstructTerm t[0]!
+    let y : Q(Int) ← reconstructTerm t[1]!
+    return q($x % $y)
+  | .DIVISION =>
+    let x : Q(Real) ← reconstructTerm t[0]!
+    let y : Q(Real) ← reconstructTerm t[1]!
+    return q($x / $y)
+  | .ABS =>
+    let x : Q(Int) ← reconstructTerm t[0]!
+    return q(Int.natAbs $x : Int)
+  | .LEQ =>
+    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x ≤ $y)
+  | .LT =>
+    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x < $y)
+  | .GEQ =>
+    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x ≥ $y)
+  | .GT =>
+    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x > $y)
+  | .TO_REAL =>
+    let x : Q(Int) ← reconstructTerm t[0]!
+    return q($x : Real)
+  | .TO_INTEGER =>
+    let x : Q(Real) ← reconstructTerm t[0]!
+    return q(⌊$x⌋)
+  | .IS_INTEGER =>
+    let x : Q(Real) ← reconstructTerm t[0]!
+    return q($x = ⌊$x⌋)
+  | _ => return none
+where
+  mkRealLit (n : Nat) : Q(Real) := match h : n with
+    | 0     => q(0 : Real)
+    | 1     => q(1 : Real)
+    | _ + 2 =>
+      let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo)
+      let h := mkApp3 q(@instOfNat Real) (mkRawNatLit n) q(Real.natCast) h
+      mkApp2 q(@OfNat.ofNat Real) (mkRawNatLit n) h
+
+def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
+  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
+  | _ => return none
+@[smt_proof_reconstruct] def reconstructArithProof : ProofReconstructor := fun pf => do match pf.getRule with
+  | .DSL_REWRITE => reconstructRewrite pf
+  | _ => return none
+
+end Smt.Reconstruct.Arith
diff --git a/Smt/Reconstruct/Arith/Reconstruct.lean b/Smt/Reconstruct/Arith/Reconstruct.lean
deleted file mode 100644
index 0c98c14e..00000000
--- a/Smt/Reconstruct/Arith/Reconstruct.lean
+++ /dev/null
@@ -1,140 +0,0 @@
-/-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
--/
-
-import Smt.Reconstruct.Arith.ArithMulSign
-import Smt.Reconstruct.Arith.MulPosNeg
-import Smt.Reconstruct.Arith.Rewrites
-import Smt.Reconstruct.Arith.SumBounds
-import Smt.Reconstruct.Arith.Rewrites
-import Smt.Reconstruct.Arith.TangentPlane
-import Smt.Reconstruct.Arith.TightBounds
-import Smt.Reconstruct.Arith.Trichotomy
-import Smt.Reconstruct.Reconstruct
-
-namespace Smt.Reconstruct.Arith
-
-open Lean hiding Rat
-open Qq
-
-@[smt_sort_reconstruct] def reconstructArithSort : SortReconstructor := fun s => do match s.getKind with
-  | .INTEGER_SORT => return q(Int)
-  | .REAL_SORT    => return q(Real)
-  | _             => return none
-
-def getTypeAndInst (s : cvc5.Sort) : Σ α : Q(Type), Q(LinearOrderedRing $α) := match s.isInteger with
-  | false => ⟨q(Real), q(Real.instLinearOrderedRingReal)⟩
-  | true  => ⟨q(Int), q(Int.linearOrderedCommRing.toLinearOrderedRing)⟩
-
-@[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
-  | .SKOLEM_FUN => match t.getSkolemId with
-    | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0)
-    | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0)
-    | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0)
-    | _ => return none
-  | .CONST_INTEGER =>
-    let x : Int := t.getIntegerValue
-    let x' : Q(Nat) := mkRawNatLit x.natAbs
-    if x ≥ 0 then
-      return q(OfNat.ofNat $x' : Int)
-    else
-      return q(-(OfNat.ofNat $x' : Int))
-  | .CONST_RATIONAL =>
-    let x : Rat := t.getRationalValue
-    let num : Q(Real) := mkRealLit x.num.natAbs
-    if x.den == 1 then
-      if x.num ≥ 0 then
-        return q($num)
-      else
-        return q(-$num)
-    else
-      let den : Q(Real) := mkRealLit x.den
-      if x.num ≥ 0 then
-        return q($num / $den)
-      else
-        return q(-$num / $den)
-  | .NEG =>
-    let ⟨α, _⟩ := getTypeAndInst t.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    return q(-$x)
-  | .SUB =>
-    let ⟨α, _⟩ := getTypeAndInst t.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x - $y)
-  | .ADD =>
-    let ⟨α, _⟩ := getTypeAndInst t.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x + $y)
-  | .MULT =>
-    let ⟨α, _⟩ := getTypeAndInst t.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x * $y)
-  | .INTS_DIVISION =>
-    let x : Q(Int) ← reconstructTerm t[0]!
-    let y : Q(Int) ← reconstructTerm t[1]!
-    return q($x / $y)
-  | .INTS_MODULUS =>
-    let x : Q(Int) ← reconstructTerm t[0]!
-    let y : Q(Int) ← reconstructTerm t[1]!
-    return q($x % $y)
-  | .DIVISION =>
-    let x : Q(Real) ← reconstructTerm t[0]!
-    let y : Q(Real) ← reconstructTerm t[1]!
-    return q($x / $y)
-  | .ABS =>
-    let x : Q(Int) ← reconstructTerm t[0]!
-    return q(Int.natAbs $x : Int)
-  | .LEQ =>
-    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x ≤ $y)
-  | .LT =>
-    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x < $y)
-  | .GEQ =>
-    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x ≥ $y)
-  | .GT =>
-    let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x > $y)
-  | .TO_REAL =>
-    let x : Q(Int) ← reconstructTerm t[0]!
-    return q($x : Real)
-  | .TO_INTEGER =>
-    let x : Q(Real) ← reconstructTerm t[0]!
-    return q(⌊$x⌋)
-  | .IS_INTEGER =>
-    let x : Q(Real) ← reconstructTerm t[0]!
-    return q($x = ⌊$x⌋)
-  | _ => return none
-where
-  mkRealLit (n : Nat) : Q(Real) := match h : n with
-    | 0     => q(0 : Real)
-    | 1     => q(1 : Real)
-    | _ + 2 =>
-      let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo)
-      let h := mkApp3 q(@instOfNat Real) (mkRawNatLit n) q(Real.natCast) h
-      mkApp2 q(@OfNat.ofNat Real) (mkRawNatLit n) h
-
-def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
-  | _ => return none
-
-@[smt_proof_reconstruct] def reconstructArithProof : ProofReconstructor := fun pf => do match pf.getRule with
-  | .DSL_REWRITE => reconstructRewrite pf
-  | _ => return none
-
-end Smt.Reconstruct.Arith
diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean
index b047c96c..19b03c72 100644
--- a/Smt/Reconstruct/BitVec.lean
+++ b/Smt/Reconstruct/BitVec.lean
@@ -5,4 +5,99 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.BitVec.Reconstruct
+import Smt.Reconstruct.Prop.Core
+import Smt.Reconstruct
+
+namespace Smt.Reconstruct.BitVec
+
+open Lean Qq
+
+@[smt_sort_reconstruct] def reconstructBitVecSort : SortReconstructor := fun s => do match s.getKind with
+  | .BITVECTOR_SORT =>
+    let w : Nat := s.getBitVectorSize.val
+    return q(Std.BitVec $w)
+  | _             => return none
+
+@[smt_term_reconstruct] partial def reconstructBitVec : TermReconstructor := fun t => do match t.getKind with
+  | .CONST_BITVECTOR =>
+    let w : Nat := t.getSort.getBitVectorSize.val
+    let v : Nat := (t.getBitVectorValue 10).toNat!
+    return q(Std.BitVec.ofNat $w $v)
+  | .BITVECTOR_BITOF =>
+    let w : Nat := t[0]!.getSort.getBitVectorSize.val
+    let x : Q(Std.BitVec $w) ← reconstructTerm t[0]!
+    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+    return q(«$x».getLsb $i = true)
+  | .BITVECTOR_BB_TERM =>
+    let w : Nat := t.getNumChildren
+    let bs : Q(Std.BitVec 0) := q(.nil)
+    let f (bs : Expr) (i : Nat) : ReconstructM Expr := do
+      let p : Q(Prop) ← reconstructTerm t[i]!
+      let bs : Q(Std.BitVec $i) := bs
+      let hp : Q(Decidable $p) ← synthDecidableInst t[i]!
+      return q(@Std.BitVec.cons $i (@decide $p $hp) $bs)
+    let bs : Q(Std.BitVec $w) ← (List.range w).foldlM f bs
+    return q($bs)
+  | .BITVECTOR_ADD =>
+    let w : Nat := t.getSort.getBitVectorSize.val
+    let x : Q(Std.BitVec $w) ← reconstructTerm t[0]!
+    let y : Q(Std.BitVec $w) ← reconstructTerm t[1]!
+    return q($x + $y)
+  | _ => return none
+where
+  rightAssocOpDecidableInst (op : Expr) (inst : Expr) (t : cvc5.Term) : ReconstructM Expr := do
+    let mut curr ← reconstructTerm t[t.getNumChildren - 1]!
+    let mut currInst ← synthDecidableInst t[t.getNumChildren - 1]!
+    for i in [1:t.getNumChildren] do
+      let ct := t[t.getNumChildren - i - 1]!
+      currInst := mkApp4 inst (← reconstructTerm ct) curr (← synthDecidableInst ct) currInst
+      curr := mkApp2 op (← reconstructTerm ct) curr
+    return currInst
+  synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t.getKind with
+    | .CONST_BOOLEAN => return if t.getBooleanValue then q(instDecidableTrue) else q(instDecidableFalse)
+    | .NOT =>
+      let p : Q(Prop) ← reconstructTerm t[0]!
+      let hp : Q(Decidable $p) ← synthDecidableInst t[0]!
+      return q(@instDecidableNot $p $hp)
+    | .AND => rightAssocOpDecidableInst q(And) q(@instDecidableAnd) t
+    | .OR => rightAssocOpDecidableInst q(Or) q(@instDecidableOr) t
+    | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidableXOr) t
+    | .EQUAL =>
+      if t[0]!.getSort.getKind == .BOOLEAN_SORT then
+        let p : Q(Prop) ← reconstructTerm t[0]!
+        let q : Q(Prop) ← reconstructTerm t[1]!
+        let hp : Q(Decidable $p) ← synthDecidableInst t[0]!
+        let hq : Q(Decidable $q) ← synthDecidableInst t[1]!
+        return q(@instDecidableEqProp $p $q (@instDecidableIff $p $q $hp $hq))
+      if t[0]!.getSort.getKind == .BITVECTOR_SORT then
+        let w : Nat := t[0]!.getSort.getBitVectorSize.val
+        return q(@Std.instDecidableEqBitVec $w)
+      let p : Q(Prop) ← reconstructTerm t
+      Meta.synthInstance q(Decidable $p)
+    | .BITVECTOR_BITOF =>
+      let w : Nat := t[0]!.getSort.getBitVectorSize.val
+      let x : Q(Std.BitVec $w) ← reconstructTerm t[0]!
+      let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+      return q(instDecidableEqBool («$x».getLsb $i) true)
+    | _ =>
+      let p : Q(Prop) ← reconstructTerm t
+      Meta.synthInstance q(Decidable $p)
+
+def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
+  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
+  | _ => return none
+
+@[smt_proof_reconstruct] def reconstructBitVecProof : ProofReconstructor := fun pf => do match pf.getRule with
+  | .DSL_REWRITE => reconstructRewrite pf
+  | .BV_BITBLAST_STEP =>
+    let t := pf.getArguments[0]![0]!
+    match t.getKind with
+    | .CONST_BITVECTOR =>
+      let w : Nat := t.getSort.getBitVectorSize.toNat
+      let t : Q(Std.BitVec $w) ← reconstructTerm pf.getResult[0]!
+      let t' : Q(Std.BitVec $w) ← reconstructTerm pf.getResult[1]!
+      addThm q($t = $t') q(Eq.refl $t)
+    | _ => return none
+  | _ => return none
+
+end Smt.Reconstruct.BitVec
diff --git a/Smt/Reconstruct/BitVec/Reconstruct.lean b/Smt/Reconstruct/BitVec/Reconstruct.lean
deleted file mode 100644
index 0f1d116f..00000000
--- a/Smt/Reconstruct/BitVec/Reconstruct.lean
+++ /dev/null
@@ -1,103 +0,0 @@
-/-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
--/
-
-import Smt.Reconstruct.Prop.Core
-import Smt.Reconstruct.Reconstruct
-
-namespace Smt.Reconstruct.BitVec
-
-open Lean Qq
-
-@[smt_sort_reconstruct] def reconstructBitVecSort : SortReconstructor := fun s => do match s.getKind with
-  | .BITVECTOR_SORT =>
-    let w : Nat := s.getBitVectorSize.val
-    return q(Std.BitVec $w)
-  | _             => return none
-
-@[smt_term_reconstruct] partial def reconstructBitVec : TermReconstructor := fun t => do match t.getKind with
-  | .CONST_BITVECTOR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let v : Nat := (t.getBitVectorValue 10).toNat!
-    return q(Std.BitVec.ofNat $w $v)
-  | .BITVECTOR_BITOF =>
-    let w : Nat := t[0]!.getSort.getBitVectorSize.val
-    let x : Q(Std.BitVec $w) ← reconstructTerm t[0]!
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
-    return q(«$x».getLsb $i = true)
-  | .BITVECTOR_BB_TERM =>
-    let w : Nat := t.getNumChildren
-    let bs : Q(Std.BitVec 0) := q(.nil)
-    let f (bs : Expr) (i : Nat) : ReconstructM Expr := do
-      let p : Q(Prop) ← reconstructTerm t[i]!
-      let bs : Q(Std.BitVec $i) := bs
-      let hp : Q(Decidable $p) ← synthDecidableInst t[i]!
-      return q(@Std.BitVec.cons $i (@decide $p $hp) $bs)
-    let bs : Q(Std.BitVec $w) ← (List.range w).foldlM f bs
-    return q($bs)
-  | .BITVECTOR_ADD =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let x : Q(Std.BitVec $w) ← reconstructTerm t[0]!
-    let y : Q(Std.BitVec $w) ← reconstructTerm t[1]!
-    return q($x + $y)
-  | _ => return none
-where
-  rightAssocOpDecidableInst (op : Expr) (inst : Expr) (t : cvc5.Term) : ReconstructM Expr := do
-    let mut curr ← reconstructTerm t[t.getNumChildren - 1]!
-    let mut currInst ← synthDecidableInst t[t.getNumChildren - 1]!
-    for i in [1:t.getNumChildren] do
-      let ct := t[t.getNumChildren - i - 1]!
-      currInst := mkApp4 inst (← reconstructTerm ct) curr (← synthDecidableInst ct) currInst
-      curr := mkApp2 op (← reconstructTerm ct) curr
-    return currInst
-  synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t.getKind with
-    | .CONST_BOOLEAN => return if t.getBooleanValue then q(instDecidableTrue) else q(instDecidableFalse)
-    | .NOT =>
-      let p : Q(Prop) ← reconstructTerm t[0]!
-      let hp : Q(Decidable $p) ← synthDecidableInst t[0]!
-      return q(@instDecidableNot $p $hp)
-    | .AND => rightAssocOpDecidableInst q(And) q(@instDecidableAnd) t
-    | .OR => rightAssocOpDecidableInst q(Or) q(@instDecidableOr) t
-    | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidableXOr) t
-    | .EQUAL =>
-      if t[0]!.getSort.getKind == .BOOLEAN_SORT then
-        let p : Q(Prop) ← reconstructTerm t[0]!
-        let q : Q(Prop) ← reconstructTerm t[1]!
-        let hp : Q(Decidable $p) ← synthDecidableInst t[0]!
-        let hq : Q(Decidable $q) ← synthDecidableInst t[1]!
-        return q(@instDecidableEqProp $p $q (@instDecidableIff $p $q $hp $hq))
-      if t[0]!.getSort.getKind == .BITVECTOR_SORT then
-        let w : Nat := t[0]!.getSort.getBitVectorSize.val
-        return q(@Std.instDecidableEqBitVec $w)
-      let p : Q(Prop) ← reconstructTerm t
-      Meta.synthInstance q(Decidable $p)
-    | .BITVECTOR_BITOF =>
-      let w : Nat := t[0]!.getSort.getBitVectorSize.val
-      let x : Q(Std.BitVec $w) ← reconstructTerm t[0]!
-      let i : Nat := t.getOp[0]!.getIntegerValue.toNat
-      return q(instDecidableEqBool («$x».getLsb $i) true)
-    | _ =>
-      let p : Q(Prop) ← reconstructTerm t
-      Meta.synthInstance q(Decidable $p)
-
-def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
-  | _ => return none
-
-@[smt_proof_reconstruct] def reconstructBitVecProof : ProofReconstructor := fun pf => do match pf.getRule with
-  | .DSL_REWRITE => reconstructRewrite pf
-  | .BV_BITBLAST_STEP =>
-    let t := pf.getArguments[0]![0]!
-    match t.getKind with
-    | .CONST_BITVECTOR =>
-      let w : Nat := t.getSort.getBitVectorSize.toNat
-      let t : Q(Std.BitVec $w) ← reconstructTerm pf.getResult[0]!
-      let t' : Q(Std.BitVec $w) ← reconstructTerm pf.getResult[1]!
-      addThm q($t = $t') q(Eq.refl $t)
-    | _ => return none
-  | _ => return none
-
-end Smt.Reconstruct.BitVec
diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean
index 44d7ef1b..6ea8e5a8 100644
--- a/Smt/Reconstruct/Builtin.lean
+++ b/Smt/Reconstruct/Builtin.lean
@@ -5,4 +5,211 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.Builtin.Reconstruct
+import Smt.Reconstruct.Builtin.Lemmas
+import Smt.Reconstruct.Builtin.Rewrites
+import Smt.Reconstruct
+
+namespace Smt.Reconstruct.Builtin
+
+open Lean Qq
+
+def getFVarExpr! (n : Name) : MetaM Expr := do
+  match (← getLCtx).findFromUserName? n with
+  | some d => return d.toExpr
+  | none   => throwError "unknown free variable '{n}'"
+
+def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
+  match (← getLCtx).findFromUserName? n with
+  | some d => return d.toExpr
+  | none   =>
+    let c ← getConstInfo n
+    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+
+@[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
+  | .VARIABLE => getFVarExpr! (getVariableName t)
+  | .CONSTANT => getFVarOrConstExpr! t.getSymbol
+  | .ITE =>
+    let α : Q(Type) ← reconstructSort t.getSort
+    let c : Q(Prop) ← reconstructTerm t[0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let x : Q($α) ← reconstructTerm t[1]!
+    let y : Q($α) ← reconstructTerm t[2]!
+    return q(@ite $α $c $h $x $y)
+  | .SKOLEM_FUN => match t.getSkolemId with
+    | .PURIFY => reconstructTerm t.getSkolemArguments[0]!
+    | _ => return none
+  | _ => return none
+where
+  getVariableName (t : cvc5.Term) : Name :=
+    if t.hasSymbol then t.getSymbol else Name.num `x t.getId
+
+def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
+  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
+  | .ITE_TRUE_COND =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[1]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[2]!
+    addThm q(ite True $x $y = $x) q(@Builtin.ite_true_cond $α $x $y)
+  | .ITE_FALSE_COND =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[1]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[2]!
+    addThm q(ite False $x $y = $y) q(@Builtin.ite_false_cond $α $x $y)
+  | .ITE_NOT_COND =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite (¬$c) $x $y = ite $c $y $x) q(@Builtin.ite_not_cond $c $α $x $y $h)
+  | .ITE_EQ_BRANCH =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $x $x = $x) q(@Builtin.ite_eq_branch $c $α $x $h)
+  | .ITE_THEN_LOOKAHEAD =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
+    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c (ite $c $x $y) $z = ite $c $x $z) q(@Builtin.ite_then_lookahead $c $α $x $y $z $h)
+  | .ITE_ELSE_LOOKAHEAD =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
+    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $x (ite $c $y $z) = ite $c $x $z) q(@Builtin.ite_else_lookahead $c $α $x $y $z $h)
+  | .ITE_THEN_NEG_LOOKAHEAD =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
+    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c (ite (¬$c) $x $y) $z = ite $c $y $z) q(@Builtin.ite_then_neg_lookahead $c $α $x $y $z $h)
+  | .ITE_ELSE_NEG_LOOKAHEAD =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
+    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
+    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $x (ite (¬$c) $y $z) = ite $c $x $y) q(@Builtin.ite_else_neg_lookahead $c $α $x $y $z $h)
+  | _ => return none
+
+@[smt_proof_reconstruct] def reconstructBuiltinProof : ProofReconstructor := fun pf => do match pf.getRule with
+  | .ASSUME =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]!
+    match (← Meta.findLocalDeclWithType? p) with
+    | none => throwError "no assumption of type\n\t{p}\nfound in local context"
+    | some fv => return Expr.fvar fv
+  | .SCOPE =>
+    let mv ← getCurrGoal
+    mv.withContext do
+      let f := fun arg ps => do
+        let p : Q(Prop) ← reconstructTerm arg
+        return q($p :: $ps)
+      let ps : Q(List Prop) ← pf.getArguments.foldrM f q([])
+      let as ← pf.getArguments.mapM (fun _ => return Name.num `a (← incCount))
+      let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
+      let h₁ : Q(impliesN $ps $q) ← Meta.mkFreshExprMVar q(impliesN $ps $q)
+      let (fvs, mv') ← h₁.mvarId!.introN pf.getArguments.size as.toList
+      setCurrGoal mv'
+      mv'.withContext do
+        let h₂ : Q($q) ← withAssums (fvs.map Expr.fvar) (reconstructProof pf.getChildren[0]!)
+        let mv'' ← getCurrGoal
+        mv''.withContext (mv''.assignIfDefeq h₂)
+      setCurrGoal mv
+      addThm q(andN $ps → $q) q(Builtin.scopes $h₁)
+  | .EVALUATE =>
+    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
+    if (← reconstructTerm pf.getResult).getUsedConstants.any (isNoncomputable (← getEnv)) then
+      return none
+    -- TODO: handle case where a Prop is inside an expression
+    if α.isProp then
+      let p  : Q(Prop) ← reconstructTerm pf.getResult[0]!
+      let p' : Q(Prop) ← reconstructTerm pf.getResult[1]!
+      let h : Q(Decidable ($p = $p')) ← Meta.synthInstance q(Decidable ($p = $p'))
+      addThm q($p = $p') (.app q(@of_decide_eq_true ($p = $p') $h) q(Eq.refl true))
+    else
+      let t  : Q($α) ← reconstructTerm pf.getResult[0]!
+      let t' : Q($α) ← reconstructTerm pf.getResult[1]!
+      addThm q($t = $t') q(Eq.refl $t)
+  | .DSL_REWRITE => reconstructRewrite pf
+  | .ITE_ELIM1 =>
+    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
+    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
+    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[2]!
+    let h : Q(@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$c ∨ $p) q(Builtin.iteElim1 $h)
+  | .ITE_ELIM2 =>
+    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
+    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
+    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[2]!
+    let h : Q(@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q($c ∨ $q) q(Builtin.iteElim2 $h)
+  | .NOT_ITE_ELIM1 =>
+    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
+    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![2]!
+    let hn : Q(¬@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$c ∨ ¬$p) q(Builtin.notIteElim1 $hn)
+  | .NOT_ITE_ELIM2 =>
+    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
+    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![2]!
+    let hn : Q(¬@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q($c ∨ ¬$q) q(Builtin.notIteElim2 $hn)
+  | .CNF_ITE_POS1 =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
+    addThm q(¬(ite $c $p $q) ∨ ¬$c ∨ $p) q(@Builtin.cnfItePos1 $c $p $q $h)
+  | .CNF_ITE_POS2 =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
+    addThm q(¬(ite $c $p $q) ∨ $c ∨ $q) q(@Builtin.cnfItePos2 $c $p $q $h)
+  | .CNF_ITE_POS3 =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
+    addThm q(¬(ite $c $p $q) ∨ $p ∨ $q) q(@Builtin.cnfItePos3 $c $p $q $h)
+  | .CNF_ITE_NEG1 =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
+    addThm q(ite $c $p $q ∨ ¬$c ∨ ¬$p) q(@Builtin.cnfIteNeg1 $c $p $q $h)
+  | .CNF_ITE_NEG2 =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
+    addThm q(ite $c $p $q ∨ $c ∨ ¬$q) q(@Builtin.cnfIteNeg2 $c $p $q $h)
+  | .CNF_ITE_NEG3 =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
+    addThm q(ite $c $p $q ∨ ¬$p ∨ ¬$q) q(@Builtin.cnfIteNeg3 $c $p $q $h)
+  | .SKOLEM_INTRO =>
+    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
+    let k : Q($α) ← reconstructTerm pf.getResult[0]!
+    let t : Q($α) ← reconstructTerm pf.getResult[1]!
+    addThm q($k = $t) q(Eq.refl $t)
+  | _ => return none
+
+end Smt.Reconstruct.Builtin
diff --git a/Smt/Reconstruct/Builtin/Reconstruct.lean b/Smt/Reconstruct/Builtin/Reconstruct.lean
deleted file mode 100644
index 01b282d4..00000000
--- a/Smt/Reconstruct/Builtin/Reconstruct.lean
+++ /dev/null
@@ -1,215 +0,0 @@
-/-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
--/
-
-import Smt.Reconstruct.Builtin.Lemmas
-import Smt.Reconstruct.Builtin.Rewrites
-import Smt.Reconstruct.Reconstruct
-
-namespace Smt.Reconstruct.Builtin
-
-open Lean Qq
-
-def getFVarExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   => throwError "unknown free variable '{n}'"
-
-def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   =>
-    let c ← getConstInfo n
-    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
-
-@[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
-  | .VARIABLE => getFVarExpr! (getVariableName t)
-  | .CONSTANT => getFVarOrConstExpr! t.getSymbol
-  | .ITE =>
-    let α : Q(Type) ← reconstructSort t.getSort
-    let c : Q(Prop) ← reconstructTerm t[0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let x : Q($α) ← reconstructTerm t[1]!
-    let y : Q($α) ← reconstructTerm t[2]!
-    return q(@ite $α $c $h $x $y)
-  | .SKOLEM_FUN => match t.getSkolemId with
-    | .PURIFY => reconstructTerm t.getSkolemArguments[0]!
-    | _ => return none
-  | _ => return none
-where
-  getVariableName (t : cvc5.Term) : Name :=
-    if t.hasSymbol then t.getSymbol else Name.num `x t.getId
-
-def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
-  | .ITE_TRUE_COND =>
-    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[1]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[2]!
-    addThm q(ite True $x $y = $x) q(@Builtin.ite_true_cond $α $x $y)
-  | .ITE_FALSE_COND =>
-    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[1]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[2]!
-    addThm q(ite False $x $y = $y) q(@Builtin.ite_false_cond $α $x $y)
-  | .ITE_NOT_COND =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite (¬$c) $x $y = ite $c $y $x) q(@Builtin.ite_not_cond $c $α $x $y $h)
-  | .ITE_EQ_BRANCH =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $x $x = $x) q(@Builtin.ite_eq_branch $c $α $x $h)
-  | .ITE_THEN_LOOKAHEAD =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
-    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c (ite $c $x $y) $z = ite $c $x $z) q(@Builtin.ite_then_lookahead $c $α $x $y $z $h)
-  | .ITE_ELSE_LOOKAHEAD =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
-    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $x (ite $c $y $z) = ite $c $x $z) q(@Builtin.ite_else_lookahead $c $α $x $y $z $h)
-  | .ITE_THEN_NEG_LOOKAHEAD =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
-    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c (ite (¬$c) $x $y) $z = ite $c $y $z) q(@Builtin.ite_then_neg_lookahead $c $α $x $y $z $h)
-  | .ITE_ELSE_NEG_LOOKAHEAD =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
-    let x : Q($α) ← reconstructTerm pf.getArguments[2]!
-    let y : Q($α) ← reconstructTerm pf.getArguments[3]!
-    let z : Q($α) ← reconstructTerm pf.getArguments[4]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $x (ite (¬$c) $y $z) = ite $c $x $y) q(@Builtin.ite_else_neg_lookahead $c $α $x $y $z $h)
-  | _ => return none
-
-@[smt_proof_reconstruct] def reconstructBuiltinProof : ProofReconstructor := fun pf => do match pf.getRule with
-  | .ASSUME =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]!
-    match (← Meta.findLocalDeclWithType? p) with
-    | none => throwError "no assumption of type\n\t{p}\nfound in local context"
-    | some fv => return Expr.fvar fv
-  | .SCOPE =>
-    let mv ← getCurrGoal
-    mv.withContext do
-      let f := fun arg ps => do
-        let p : Q(Prop) ← reconstructTerm arg
-        return q($p :: $ps)
-      let ps : Q(List Prop) ← pf.getArguments.foldrM f q([])
-      let as ← pf.getArguments.mapM (fun _ => return Name.num `a (← incCount))
-      let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
-      let h₁ : Q(impliesN $ps $q) ← Meta.mkFreshExprMVar q(impliesN $ps $q)
-      let (fvs, mv') ← h₁.mvarId!.introN pf.getArguments.size as.toList
-      setCurrGoal mv'
-      mv'.withContext do
-        let h₂ : Q($q) ← withAssums (fvs.map Expr.fvar) (reconstructProof pf.getChildren[0]!)
-        let mv'' ← getCurrGoal
-        mv''.withContext (mv''.assignIfDefeq h₂)
-      setCurrGoal mv
-      addThm q(andN $ps → $q) q(Builtin.scopes $h₁)
-  | .EVALUATE =>
-    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
-    if (← reconstructTerm pf.getResult).getUsedConstants.any (isNoncomputable (← getEnv)) then
-      return none
-    -- TODO: handle case where a Prop is inside an expression
-    if α.isProp then
-      let p  : Q(Prop) ← reconstructTerm pf.getResult[0]!
-      let p' : Q(Prop) ← reconstructTerm pf.getResult[1]!
-      let h : Q(Decidable ($p = $p')) ← Meta.synthInstance q(Decidable ($p = $p'))
-      addThm q($p = $p') (.app q(@of_decide_eq_true ($p = $p') $h) q(Eq.refl true))
-    else
-      let t  : Q($α) ← reconstructTerm pf.getResult[0]!
-      let t' : Q($α) ← reconstructTerm pf.getResult[1]!
-      addThm q($t = $t') q(Eq.refl $t)
-  | .DSL_REWRITE => reconstructRewrite pf
-  | .ITE_ELIM1 =>
-    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
-    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
-    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[2]!
-    let h : Q(@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$c ∨ $p) q(Builtin.iteElim1 $h)
-  | .ITE_ELIM2 =>
-    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
-    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
-    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[2]!
-    let h : Q(@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q($c ∨ $q) q(Builtin.iteElim2 $h)
-  | .NOT_ITE_ELIM1 =>
-    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
-    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![2]!
-    let hn : Q(¬@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$c ∨ ¬$p) q(Builtin.notIteElim1 $hn)
-  | .NOT_ITE_ELIM2 =>
-    let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
-    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![2]!
-    let hn : Q(¬@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q($c ∨ ¬$q) q(Builtin.notIteElim2 $hn)
-  | .CNF_ITE_POS1 =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
-    addThm q(¬(ite $c $p $q) ∨ ¬$c ∨ $p) q(@Builtin.cnfItePos1 $c $p $q $h)
-  | .CNF_ITE_POS2 =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
-    addThm q(¬(ite $c $p $q) ∨ $c ∨ $q) q(@Builtin.cnfItePos2 $c $p $q $h)
-  | .CNF_ITE_POS3 =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
-    addThm q(¬(ite $c $p $q) ∨ $p ∨ $q) q(@Builtin.cnfItePos3 $c $p $q $h)
-  | .CNF_ITE_NEG1 =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
-    addThm q(ite $c $p $q ∨ ¬$c ∨ ¬$p) q(@Builtin.cnfIteNeg1 $c $p $q $h)
-  | .CNF_ITE_NEG2 =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
-    addThm q(ite $c $p $q ∨ $c ∨ ¬$q) q(@Builtin.cnfIteNeg2 $c $p $q $h)
-  | .CNF_ITE_NEG3 =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
-    addThm q(ite $c $p $q ∨ ¬$p ∨ ¬$q) q(@Builtin.cnfIteNeg3 $c $p $q $h)
-  | .SKOLEM_INTRO =>
-    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
-    let k : Q($α) ← reconstructTerm pf.getResult[0]!
-    let t : Q($α) ← reconstructTerm pf.getResult[1]!
-    addThm q($k = $t) q(Eq.refl $t)
-  | _ => return none
-
-end Smt.Reconstruct.Builtin
diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean
index c3245456..243e3000 100644
--- a/Smt/Reconstruct/Prop.lean
+++ b/Smt/Reconstruct/Prop.lean
@@ -5,4 +5,458 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.Prop.Reconstruct
+import Smt.Reconstruct.Prop.Core
+import Smt.Reconstruct.Prop.Factor
+import Smt.Reconstruct.Prop.Lemmas
+import Smt.Reconstruct.Prop.LiftOrNToImp
+import Smt.Reconstruct.Prop.LiftOrNToNeg
+import Smt.Reconstruct.Prop.PermutateOr
+import Smt.Reconstruct.Prop.Pull
+import Smt.Reconstruct.Prop.Resolution
+import Smt.Reconstruct.Prop.Rewrites
+import Smt.Reconstruct
+import Smt.Reconstruct.Rewrite
+
+namespace Smt.Reconstruct.Prop
+
+open Lean Qq
+
+@[smt_sort_reconstruct] def reconstructSort : SortReconstructor := fun s => do match s.getKind with
+  | .BOOLEAN_SORT => return q(Prop)
+  | _             => return none
+
+@[smt_term_reconstruct] def reconstructProp : TermReconstructor := fun t => do match t.getKind with
+  | .CONST_BOOLEAN => return if t.getBooleanValue then q(True) else q(False)
+  | .NOT =>
+    let b : Q(Prop) ← reconstructTerm t[0]!
+    return q(¬$b)
+  | .IMPLIES =>
+    let mut curr : Q(Prop) ← reconstructTerm t[t.getNumChildren - 1]!
+    for i in [1:t.getNumChildren] do
+      let p : Q(Prop) ← reconstructTerm t[t.getNumChildren - i - 1]!
+      curr := q($p → $curr)
+    return curr
+  | .AND => rightAssocOp q(And) t
+  | .OR => rightAssocOp q(Or) t
+  | .XOR => rightAssocOp q(XOr) t
+  | _ => return none
+where
+  rightAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do
+    let mut curr ← reconstructTerm t[t.getNumChildren - 1]!
+    for i in [1:t.getNumChildren] do
+      curr := mkApp2 op (← reconstructTerm t[t.getNumChildren - i - 1]!) curr
+    return curr
+
+def reconstructRewrite (pf : cvc5.Proof) (cpfs : Array Expr) : ReconstructM (Option Expr) := do
+  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
+  | .BOOL_DOUBLE_NOT_ELIM =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q((¬¬$p) = $p) q(@Prop.bool_double_not_elim $p)
+  | .BOOL_EQ_TRUE =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(($p = True) = $p) q(@Prop.bool_eq_true $p)
+  | .BOOL_EQ_FALSE =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(($p = False) = ¬$p) q(@Prop.bool_eq_false $p)
+  | .BOOL_EQ_NREFL =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(($p = ¬$p) = False) q(@Prop.bool_eq_nrefl $p)
+  | .BOOL_IMPL_FALSE1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(($p → False) = ¬$p) q(@Prop.bool_impl_false1 $p)
+  | .BOOL_IMPL_FALSE2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q((False → $p) = True) q(@Prop.bool_impl_false2 $p)
+  | .BOOL_IMPL_TRUE1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(($p → True) = True) q(@Prop.bool_impl_true1 $p)
+  | .BOOL_IMPL_TRUE2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q((True → $p) = $p) q(@Prop.bool_impl_true2 $p)
+  -- | .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_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)
+  | .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)
+  | .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)
+  | .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)
+  | .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)
+  | .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)
+  | .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)
+  | .BOOL_XOR_REFL =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p)
+  | .BOOL_XOR_NREFL =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q((XOr $p ¬$p) = True) q(@Prop.bool_xor_nrefl $p)
+  | .BOOL_XOR_FALSE =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(XOr $p False = $p) q(@Prop.bool_xor_false $p)
+  | .BOOL_XOR_TRUE =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    addThm q(XOr $p True = ¬$p) q(@Prop.bool_xor_true $p)
+  | .BOOL_XOR_COMM =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    addThm q(XOr $p $q = XOr $q $p) q(@Prop.bool_xor_comm $p $q)
+  | .BOOL_XOR_ELIM =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    addThm q(XOr $p $q = ¬($p = $q)) q(@Prop.bool_xor_elim $p $q)
+  | .ITE_NEG_BRANCH =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[3]!
+    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let h : Q($p = ¬$q) := cpfs[0]!
+    addThm q(ite $c $p $q = ($c = $p)) q(@Prop.ite_neg_branch $c $p $q $hc $h)
+  | .ITE_THEN_TRUE =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c True $p = ($c ∨ $p)) q(@Prop.ite_then_true $c $p $h)
+  | .ITE_ELSE_FALSE =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $p False = ($c ∧ $p)) q(@Prop.ite_else_false $c $p $h)
+  | .ITE_THEN_FALSE =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c False $p = (¬$c ∧ $p)) q(@Prop.ite_then_false $c $p $h)
+  | .ITE_ELSE_TRUE =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $p True = (¬$c ∨ $p)) q(@Prop.ite_else_true $c $p $h)
+  | .ITE_THEN_LOOKAHEAD_SELF =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $c $p = ite $c True $p) q(@Prop.ite_then_lookahead_self $c $p $h)
+  | .ITE_ELSE_LOOKAHEAD_SELF =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $p $c = ite $c $p False) q(@Prop.ite_else_lookahead_self $c $p $h)
+  | _ => return none
+where
+  reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do
+    let mut args' := #[]
+    for arg in args do
+      let mut arg' := #[]
+      for subarg in arg do
+        arg' := arg'.push (← reconstructTerm subarg)
+      args' := args'.push arg'
+    return args'
+
+def getResolutionResult (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) : Array cvc5.Term := Id.run do
+  let l₁ := if pol.getBooleanValue then l else l.not
+  let l₂ := if pol.getBooleanValue then l.not else l
+  let mut ls := #[]
+  for li in c₁ do
+    if li != l₁ then
+      ls := ls.push li
+  for li in c₂ do
+    if li != l₂ then
+      ls := ls.push li
+  return ls
+
+def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (p₁ p₂ : Expr) : ReconstructM Expr := do
+  let f := if pol.getBooleanValue == true then r₀ else r₁
+  addTac (← rightAssocOp q(Or) (getResolutionResult c₁ c₂ pol l)) (f · p₁ p₂ (← reconstructTerm l) (some (c₁.size - 1)) (some (c₂.size - 1)))
+where
+  rightAssocOp (op : Expr) (ts : Array cvc5.Term) : ReconstructM Expr := do
+    if ts.isEmpty then
+      return q(False)
+    let mut curr ← reconstructTerm ts[ts.size - 1]!
+    for i in [1:ts.size] do
+      curr := mkApp2 op (← reconstructTerm ts[ts.size - i - 1]!) curr
+    return curr
+
+def clausify (c : cvc5.Term) : Array cvc5.Term := Id.run do
+  if c.getKind != .OR then
+    return #[c]
+  let mut cs := #[]
+  for cc in c do
+    cs := cs.push cc
+  return cs
+
+def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : ReconstructM Expr := do
+  let mut cc := clausify cs[0]!
+  let mut cp := ps[0]!
+  for i in [1:cs.size] do
+    let pol := as[0]![i - 1]!
+    let l := as[1]![i - 1]!
+    cp ← reconstructResolution cc (clausify cs[i]!) pol l cp ps[i]!
+    cc := getResolutionResult cc (clausify cs[i]!) pol l
+  return cp
+
+@[smt_proof_reconstruct] def reconstructPropProof : ProofReconstructor := fun pf => do match pf.getRule with
+  | .DSL_REWRITE => reconstructRewrite pf (← pf.getChildren.mapM reconstructProof)
+  | .RESOLUTION =>
+    let c₁ := clausify pf.getChildren[0]!.getResult
+    let c₂ := clausify pf.getChildren[1]!.getResult
+    let p₁ ← reconstructProof pf.getChildren[0]!
+    let p₂ ← reconstructProof pf.getChildren[1]!
+    reconstructResolution c₁ c₂ pf.getArguments[0]! pf.getArguments[1]! p₁ p₂
+  | .CHAIN_RESOLUTION =>
+    let cs := pf.getChildren.map (·.getResult)
+    let as := pf.getArguments
+    let ps ← pf.getChildren.mapM reconstructProof
+    reconstructChainResolution cs as ps
+  | .FACTORING =>
+    -- as an argument we pass whether the suffix of the factoring clause is a
+    -- singleton *repeated* literal. This is marked by a number as in
+    -- resolution.
+    let children := pf.getChildren
+    let lastPremiseLit := children[0]!.getResult[children[0]!.getResult.getNumChildren - 1]!
+    let resOriginal := pf.getResult
+    -- For the last premise literal to be a singleton repeated literal, either
+    -- it is equal to the result (in which case the premise was just n
+    -- occurrences of it), or the end of the original clause is different from
+    -- the end of the resulting one. In principle we'd need to add the
+    -- singleton information only for OR nodes, so we could avoid this test if
+    -- the result is not an OR node. However given the presence of
+    -- purification boolean variables which can stand for OR nodes (and could
+    -- thus be ambiguous in the final step, with the purification remove), we
+    -- do the general test.
+    let singleton := if lastPremiseLit == resOriginal || (resOriginal.getKind == .OR && lastPremiseLit != resOriginal[resOriginal.getNumChildren - 1]!)
+      then some (children[0]!.getResult.getNumChildren - 1) else none;
+    addTac (← reconstructTerm pf.getResult) (factor · (← reconstructProof children[0]!) singleton)
+  | .REORDERING =>
+    let children := pf.getChildren
+    let size := pf.getResult.getNumChildren
+    let lastPremiseLit := children[0]!.getResult[size - 1]!
+    -- none if tail of the clause is not an OR (i.e., it cannot be a singleton)
+    let singleton := if lastPremiseLit.getKind == .OR then some (size - 1) else none
+    -- for each literal in the resulting clause, get its position in the premise
+    let mut pos := #[]
+    for resLit in pf.getResult do
+      for i in [:size] do
+        if children[0]!.getResult[i]! == resLit then
+          pos := pos.push i
+    -- turn conclusion into clause
+    addTac (← reconstructTerm pf.getResult) (reorder · (← reconstructProof children[0]!) pos singleton)
+  | .SPLIT =>
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]!
+    addThm q($q ∨ ¬$q) q(Classical.em $q)
+  | .EQ_RESOLVE =>
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
+    let q : Q(Prop) ← reconstructTerm pf.getResult
+    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
+    let hpq : Q($p = $q) ← reconstructProof pf.getChildren[1]!
+    addThm q($q) q(Prop.eqResolve $hp $hpq)
+  | .MODUS_PONENS =>
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
+    let q : Q(Prop) ← reconstructTerm pf.getResult
+    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
+    let hpq : Q($p → $q) ← reconstructProof pf.getChildren[1]!
+    addThm q($q) q(Prop.modusPonens $hp $hpq)
+  | .NOT_NOT_ELIM =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult
+    let hnnp : Q(¬¬$p) ← reconstructProof pf.getChildren[0]!
+    addThm q($p) q(Prop.notNotElim $hnnp)
+  | .CONTRA =>
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
+    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
+    let hnp : Q(¬$p) ← reconstructProof pf.getChildren[0]!
+    addThm q(False) q(Prop.contradiction $hp $hnp)
+  | .AND_ELIM =>
+    addTac (← reconstructTerm pf.getResult) (andElim · (← reconstructProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat)
+  | .AND_INTRO =>
+    let cpfs := pf.getChildren
+    let q : Q(Prop) ← reconstructTerm cpfs.back.getResult
+    let hq : Q($q) ← reconstructProof cpfs.back
+    let f := fun pf ⟨q, hq⟩ => do
+      let p : Q(Prop) ← reconstructTerm pf.getResult
+      let hp : Q($p) ← reconstructProof pf
+      let hq ← addThm q($p ∧ $q) q(And.intro $hp $hq)
+      let q := q($p ∧ $q)
+      return ⟨q, hq⟩
+    let ⟨_, hq⟩ ← cpfs.pop.foldrM f (⟨q, hq⟩ : Σ q : Q(Prop), Q($q))
+    return hq
+  | .NOT_OR_ELIM =>
+    addTac (← reconstructTerm pf.getResult) (notOrElim · (← reconstructProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat)
+  | .IMPLIES_ELIM =>
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
+    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
+    let hpq : Q($p → $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$p ∨ $q) q(Prop.impliesElim $hpq)
+  | .NOT_IMPLIES_ELIM1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult
+    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]!
+    let hnpq : Q(¬($p → $q)) ← reconstructProof pf.getChildren[0]!
+    addThm q($p) q(Prop.notImplies1 $hnpq)
+  | .NOT_IMPLIES_ELIM2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let hnpq : Q(¬($p → $q)) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$q) q(Prop.notImplies2 $hnpq)
+  | .EQUIV_ELIM1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
+    let hpq : Q($p = $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$p ∨ $q) q(Prop.equivElim1 $hpq)
+  | .EQUIV_ELIM2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
+    let hpq : Q($p = $q) ← reconstructProof pf.getChildren[0]!
+    addThm q($p ∨ ¬$q) q(Prop.equivElim2 $hpq)
+  | .NOT_EQUIV_ELIM1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
+    let hnpq : Q($p ≠ $q) ← reconstructProof pf.getChildren[0]!
+    addThm q($p ∨ $q) q(Prop.notEquivElim1 $hnpq)
+  | .NOT_EQUIV_ELIM2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
+    let hnpq : Q($p ≠ $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$p ∨ ¬$q) q(Prop.notEquivElim2 $hnpq)
+  | .XOR_ELIM1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
+    let hpq : Q(XOr $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q($p ∨ $q) q(Prop.xorElim1 $hpq)
+  | .XOR_ELIM2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
+    let hpq : Q(XOr $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$p ∨ ¬$q) q(Prop.xorElim2 $hpq)
+  | .NOT_XOR_ELIM1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
+    let hnpq : Q(¬XOr $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q($p ∨ ¬$q) q(Prop.notXorElim1 $hnpq)
+  | .NOT_XOR_ELIM2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
+    let hnpq : Q(¬XOr $p $q) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$p ∨ $q) q(Prop.notXorElim2 $hnpq)
+  | .NOT_AND =>
+    let fs := pf.getChildren[0]!.getResult[0]!
+    let mut ps : Q(List Prop) := q([])
+    let n := fs.getNumChildren
+    for i in [:n] do
+      let p : Q(Prop) ← reconstructTerm fs[n - i - 1]!
+      ps := q($p :: $ps)
+    let hnps : Q(¬andN $ps) ← reconstructProof pf.getChildren[0]!
+    addThm (← reconstructTerm pf.getResult) (.app q(Prop.notAnd $ps) hnps)
+  | .CNF_AND_POS =>
+    let cnf := pf.getArguments[0]!
+    let i : Nat := pf.getArguments[1]!.getIntegerValue.toNat
+    let mut ps : Q(List Prop) := q([])
+    let n := cnf.getNumChildren
+    for i in [:n] do
+      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
+      ps := q($p :: $ps)
+    addThm (← reconstructTerm pf.getResult) q(Prop.cnfAndPos $ps $i)
+  | .CNF_AND_NEG =>
+    let cnf := pf.getArguments[0]!
+    let mut ps : Q(List Prop) := q([])
+    let n := cnf.getNumChildren
+    for i in [:n] do
+      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
+      ps := q($p :: $ps)
+    addThm (← reconstructTerm pf.getResult) q(Prop.cnfAndNeg $ps)
+  | .CNF_OR_POS =>
+    let cnf := pf.getArguments[0]!
+    let mut ps : Q(List Prop) := q([])
+    let n := cnf.getNumChildren
+    for i in [:n] do
+      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
+      ps := q($p :: $ps)
+    addThm (← reconstructTerm pf.getResult) q(Prop.cnfOrPos $ps)
+  | .CNF_OR_NEG =>
+    let cnf := pf.getArguments[0]!
+    let i : Nat := pf.getArguments[1]!.getIntegerValue.toNat
+    let mut ps : Q(List Prop) := q([])
+    let n := cnf.getNumChildren
+    for i in [:n] do
+      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
+      ps := q($p :: $ps)
+    addThm (← reconstructTerm pf.getResult) q(Prop.cnfOrNeg $ps $i)
+  | .CNF_IMPLIES_POS =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(¬($p → $q) ∨ ¬$p ∨ $q) q(@Prop.cnfImpliesPos $p $q)
+  | .CNF_IMPLIES_NEG1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(($p → $q) ∨ $p) q(@Prop.cnfImpliesNeg1 $p $q)
+  | .CNF_IMPLIES_NEG2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(($p → $q) ∨ ¬$q) q(@Prop.cnfImpliesNeg2 $p $q)
+  | .CNF_EQUIV_POS1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q($p ≠ $q ∨ ¬$p ∨ $q) q(@Prop.cnfEquivPos1 $p $q)
+  | .CNF_EQUIV_POS2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q($p ≠ $q ∨ $p ∨ ¬$q) q(@Prop.cnfEquivPos2 $p $q)
+  | .CNF_EQUIV_NEG1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q($p = $q ∨ $p ∨ $q) q(@Prop.cnfEquivNeg1 $p $q)
+  | .CNF_EQUIV_NEG2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q($p = $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfEquivNeg2 $p $q)
+  | .CNF_XOR_POS1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(¬XOr $p $q ∨ $p ∨ $q) q(@Prop.cnfXorPos1 $p $q)
+  | .CNF_XOR_POS2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(¬XOr $p $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfXorPos2 $p $q)
+  | .CNF_XOR_NEG1 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(XOr $p $q ∨ ¬$p ∨ $q) q(@Prop.cnfXorNeg1 $p $q)
+  | .CNF_XOR_NEG2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
+    addThm q(XOr $p $q ∨ $p ∨ ¬$q) q(@Prop.cnfXorNeg2 $p $q)
+  | .TRUE_INTRO =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
+    addThm q($p = True) q(Prop.trueIntro $hp)
+  | .TRUE_ELIM =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult
+    let hp : Q($p = True) ← reconstructProof pf.getChildren[0]!
+    addThm q($p) q(Prop.trueElim $hp)
+  | .FALSE_INTRO =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let hnp : Q(¬$p) ← reconstructProof pf.getChildren[0]!
+    addThm q($p = False) q(Prop.falseIntro $hnp)
+  | .FALSE_ELIM =>
+    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
+    let hnp : Q($p = False) ← reconstructProof pf.getChildren[0]!
+    addThm q(¬$p) q(Prop.falseElim $hnp)
+  | _ => return none
+
+end Smt.Reconstruct.Prop
diff --git a/Smt/Reconstruct/Prop/Reconstruct.lean b/Smt/Reconstruct/Prop/Reconstruct.lean
deleted file mode 100644
index 838c93ea..00000000
--- a/Smt/Reconstruct/Prop/Reconstruct.lean
+++ /dev/null
@@ -1,462 +0,0 @@
-/-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
--/
-
-import Smt.Reconstruct.Prop.Core
-import Smt.Reconstruct.Prop.Factor
-import Smt.Reconstruct.Prop.Lemmas
-import Smt.Reconstruct.Prop.LiftOrNToImp
-import Smt.Reconstruct.Prop.LiftOrNToNeg
-import Smt.Reconstruct.Prop.PermutateOr
-import Smt.Reconstruct.Prop.Pull
-import Smt.Reconstruct.Prop.Resolution
-import Smt.Reconstruct.Prop.Rewrites
-import Smt.Reconstruct.Reconstruct
-import Smt.Reconstruct.Rewrite
-
-namespace Smt.Reconstruct.Prop
-
-open Lean Qq
-
-@[smt_sort_reconstruct] def reconstructSort : SortReconstructor := fun s => do match s.getKind with
-  | .BOOLEAN_SORT => return q(Prop)
-  | _             => return none
-
-@[smt_term_reconstruct] def reconstructProp : TermReconstructor := fun t => do match t.getKind with
-  | .CONST_BOOLEAN => return if t.getBooleanValue then q(True) else q(False)
-  | .NOT =>
-    let b : Q(Prop) ← reconstructTerm t[0]!
-    return q(¬$b)
-  | .IMPLIES =>
-    let mut curr : Q(Prop) ← reconstructTerm t[t.getNumChildren - 1]!
-    for i in [1:t.getNumChildren] do
-      let p : Q(Prop) ← reconstructTerm t[t.getNumChildren - i - 1]!
-      curr := q($p → $curr)
-    return curr
-  | .AND => rightAssocOp q(And) t
-  | .OR => rightAssocOp q(Or) t
-  | .XOR => rightAssocOp q(XOr) t
-  | _ => return none
-where
-  rightAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do
-    let mut curr ← reconstructTerm t[t.getNumChildren - 1]!
-    for i in [1:t.getNumChildren] do
-      curr := mkApp2 op (← reconstructTerm t[t.getNumChildren - i - 1]!) curr
-    return curr
-
-def reconstructRewrite (pf : cvc5.Proof) (cpfs : Array Expr) : ReconstructM (Option Expr) := do
-  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
-  | .BOOL_DOUBLE_NOT_ELIM =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q((¬¬$p) = $p) q(@Prop.bool_double_not_elim $p)
-  | .BOOL_EQ_TRUE =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(($p = True) = $p) q(@Prop.bool_eq_true $p)
-  | .BOOL_EQ_FALSE =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(($p = False) = ¬$p) q(@Prop.bool_eq_false $p)
-  | .BOOL_EQ_NREFL =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(($p = ¬$p) = False) q(@Prop.bool_eq_nrefl $p)
-  | .BOOL_IMPL_FALSE1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(($p → False) = ¬$p) q(@Prop.bool_impl_false1 $p)
-  | .BOOL_IMPL_FALSE2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q((False → $p) = True) q(@Prop.bool_impl_false2 $p)
-  | .BOOL_IMPL_TRUE1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(($p → True) = True) q(@Prop.bool_impl_true1 $p)
-  | .BOOL_IMPL_TRUE2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q((True → $p) = $p) q(@Prop.bool_impl_true2 $p)
-  -- | .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_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)
-  | .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)
-  | .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)
-  | .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)
-  | .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)
-  | .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)
-  | .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)
-  | .BOOL_XOR_REFL =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p)
-  | .BOOL_XOR_NREFL =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q((XOr $p ¬$p) = True) q(@Prop.bool_xor_nrefl $p)
-  | .BOOL_XOR_FALSE =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(XOr $p False = $p) q(@Prop.bool_xor_false $p)
-  | .BOOL_XOR_TRUE =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    addThm q(XOr $p True = ¬$p) q(@Prop.bool_xor_true $p)
-  | .BOOL_XOR_COMM =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    addThm q(XOr $p $q = XOr $q $p) q(@Prop.bool_xor_comm $p $q)
-  | .BOOL_XOR_ELIM =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    addThm q(XOr $p $q = ¬($p = $q)) q(@Prop.bool_xor_elim $p $q)
-  | .ITE_NEG_BRANCH =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[3]!
-    let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    let h : Q($p = ¬$q) := cpfs[0]!
-    addThm q(ite $c $p $q = ($c = $p)) q(@Prop.ite_neg_branch $c $p $q $hc $h)
-  | .ITE_THEN_TRUE =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c True $p = ($c ∨ $p)) q(@Prop.ite_then_true $c $p $h)
-  | .ITE_ELSE_FALSE =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $p False = ($c ∧ $p)) q(@Prop.ite_else_false $c $p $h)
-  | .ITE_THEN_FALSE =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c False $p = (¬$c ∧ $p)) q(@Prop.ite_then_false $c $p $h)
-  | .ITE_ELSE_TRUE =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $p True = (¬$c ∨ $p)) q(@Prop.ite_else_true $c $p $h)
-  | .ITE_THEN_LOOKAHEAD_SELF =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $c $p = ite $c True $p) q(@Prop.ite_then_lookahead_self $c $p $h)
-  | .ITE_ELSE_LOOKAHEAD_SELF =>
-    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
-    addThm q(ite $c $p $c = ite $c $p False) q(@Prop.ite_else_lookahead_self $c $p $h)
-  | _ => return none
-where
-  reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do
-    let mut args' := #[]
-    for arg in args do
-      let mut arg' := #[]
-      for subarg in arg do
-        arg' := arg'.push (← reconstructTerm subarg)
-      args' := args'.push arg'
-    return args'
-
-def getResolutionResult (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) : Array cvc5.Term := Id.run do
-  let l₁ := if pol.getBooleanValue then l else l.not
-  let l₂ := if pol.getBooleanValue then l.not else l
-  let mut ls := #[]
-  for li in c₁ do
-    if li != l₁ then
-      ls := ls.push li
-  for li in c₂ do
-    if li != l₂ then
-      ls := ls.push li
-  return ls
-
-def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (p₁ p₂ : Expr) : ReconstructM Expr := do
-  let f := if pol.getBooleanValue == true then r₀ else r₁
-  addTac (← rightAssocOp q(Or) (getResolutionResult c₁ c₂ pol l)) (f · p₁ p₂ (← reconstructTerm l) (some (c₁.size - 1)) (some (c₂.size - 1)))
-where
-  rightAssocOp (op : Expr) (ts : Array cvc5.Term) : ReconstructM Expr := do
-    if ts.isEmpty then
-      return q(False)
-    let mut curr ← reconstructTerm ts[ts.size - 1]!
-    for i in [1:ts.size] do
-      curr := mkApp2 op (← reconstructTerm ts[ts.size - i - 1]!) curr
-    return curr
-
-def clausify (c : cvc5.Term) : Array cvc5.Term := Id.run do
-  if c.getKind != .OR then
-    return #[c]
-  let mut cs := #[]
-  for cc in c do
-    cs := cs.push cc
-  return cs
-
-def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : ReconstructM Expr := do
-  let mut cc := clausify cs[0]!
-  let mut cp := ps[0]!
-  for i in [1:cs.size] do
-    let pol := as[0]![i - 1]!
-    let l := as[1]![i - 1]!
-    cp ← reconstructResolution cc (clausify cs[i]!) pol l cp ps[i]!
-    cc := getResolutionResult cc (clausify cs[i]!) pol l
-  return cp
-
-@[smt_proof_reconstruct] def reconstructPropProof : ProofReconstructor := fun pf => do match pf.getRule with
-  | .DSL_REWRITE => reconstructRewrite pf (← pf.getChildren.mapM reconstructProof)
-  | .RESOLUTION =>
-    let c₁ := clausify pf.getChildren[0]!.getResult
-    let c₂ := clausify pf.getChildren[1]!.getResult
-    let p₁ ← reconstructProof pf.getChildren[0]!
-    let p₂ ← reconstructProof pf.getChildren[1]!
-    reconstructResolution c₁ c₂ pf.getArguments[0]! pf.getArguments[1]! p₁ p₂
-  | .CHAIN_RESOLUTION =>
-    let cs := pf.getChildren.map (·.getResult)
-    let as := pf.getArguments
-    let ps ← pf.getChildren.mapM reconstructProof
-    reconstructChainResolution cs as ps
-  | .FACTORING =>
-    -- as an argument we pass whether the suffix of the factoring clause is a
-    -- singleton *repeated* literal. This is marked by a number as in
-    -- resolution.
-    let children := pf.getChildren
-    let lastPremiseLit := children[0]!.getResult[children[0]!.getResult.getNumChildren - 1]!
-    let resOriginal := pf.getResult
-    -- For the last premise literal to be a singleton repeated literal, either
-    -- it is equal to the result (in which case the premise was just n
-    -- occurrences of it), or the end of the original clause is different from
-    -- the end of the resulting one. In principle we'd need to add the
-    -- singleton information only for OR nodes, so we could avoid this test if
-    -- the result is not an OR node. However given the presence of
-    -- purification boolean variables which can stand for OR nodes (and could
-    -- thus be ambiguous in the final step, with the purification remove), we
-    -- do the general test.
-    let singleton := if lastPremiseLit == resOriginal || (resOriginal.getKind == .OR && lastPremiseLit != resOriginal[resOriginal.getNumChildren - 1]!)
-      then some (children[0]!.getResult.getNumChildren - 1) else none;
-    addTac (← reconstructTerm pf.getResult) (factor · (← reconstructProof children[0]!) singleton)
-  | .REORDERING =>
-    let children := pf.getChildren
-    let size := pf.getResult.getNumChildren
-    let lastPremiseLit := children[0]!.getResult[size - 1]!
-    -- none if tail of the clause is not an OR (i.e., it cannot be a singleton)
-    let singleton := if lastPremiseLit.getKind == .OR then some (size - 1) else none
-    -- for each literal in the resulting clause, get its position in the premise
-    let mut pos := #[]
-    for resLit in pf.getResult do
-      for i in [:size] do
-        if children[0]!.getResult[i]! == resLit then
-          pos := pos.push i
-    -- turn conclusion into clause
-    addTac (← reconstructTerm pf.getResult) (reorder · (← reconstructProof children[0]!) pos singleton)
-  | .SPLIT =>
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]!
-    addThm q($q ∨ ¬$q) q(Classical.em $q)
-  | .EQ_RESOLVE =>
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
-    let q : Q(Prop) ← reconstructTerm pf.getResult
-    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
-    let hpq : Q($p = $q) ← reconstructProof pf.getChildren[1]!
-    addThm q($q) q(Prop.eqResolve $hp $hpq)
-  | .MODUS_PONENS =>
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
-    let q : Q(Prop) ← reconstructTerm pf.getResult
-    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
-    let hpq : Q($p → $q) ← reconstructProof pf.getChildren[1]!
-    addThm q($q) q(Prop.modusPonens $hp $hpq)
-  | .NOT_NOT_ELIM =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult
-    let hnnp : Q(¬¬$p) ← reconstructProof pf.getChildren[0]!
-    addThm q($p) q(Prop.notNotElim $hnnp)
-  | .CONTRA =>
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult
-    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
-    let hnp : Q(¬$p) ← reconstructProof pf.getChildren[0]!
-    addThm q(False) q(Prop.contradiction $hp $hnp)
-  | .AND_ELIM =>
-    addTac (← reconstructTerm pf.getResult) (andElim · (← reconstructProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat)
-  | .AND_INTRO =>
-    let cpfs := pf.getChildren
-    let q : Q(Prop) ← reconstructTerm cpfs.back.getResult
-    let hq : Q($q) ← reconstructProof cpfs.back
-    let f := fun pf ⟨q, hq⟩ => do
-      let p : Q(Prop) ← reconstructTerm pf.getResult
-      let hp : Q($p) ← reconstructProof pf
-      let hq ← addThm q($p ∧ $q) q(And.intro $hp $hq)
-      let q := q($p ∧ $q)
-      return ⟨q, hq⟩
-    let ⟨_, hq⟩ ← cpfs.pop.foldrM f (⟨q, hq⟩ : Σ q : Q(Prop), Q($q))
-    return hq
-  | .NOT_OR_ELIM =>
-    addTac (← reconstructTerm pf.getResult) (notOrElim · (← reconstructProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat)
-  | .IMPLIES_ELIM =>
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
-    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
-    let hpq : Q($p → $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$p ∨ $q) q(Prop.impliesElim $hpq)
-  | .NOT_IMPLIES_ELIM1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult
-    let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]!
-    let hnpq : Q(¬($p → $q)) ← reconstructProof pf.getChildren[0]!
-    addThm q($p) q(Prop.notImplies1 $hnpq)
-  | .NOT_IMPLIES_ELIM2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let hnpq : Q(¬($p → $q)) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$q) q(Prop.notImplies2 $hnpq)
-  | .EQUIV_ELIM1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
-    let hpq : Q($p = $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$p ∨ $q) q(Prop.equivElim1 $hpq)
-  | .EQUIV_ELIM2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
-    let hpq : Q($p = $q) ← reconstructProof pf.getChildren[0]!
-    addThm q($p ∨ ¬$q) q(Prop.equivElim2 $hpq)
-  | .NOT_EQUIV_ELIM1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
-    let hnpq : Q($p ≠ $q) ← reconstructProof pf.getChildren[0]!
-    addThm q($p ∨ $q) q(Prop.notEquivElim1 $hnpq)
-  | .NOT_EQUIV_ELIM2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
-    let hnpq : Q($p ≠ $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$p ∨ ¬$q) q(Prop.notEquivElim2 $hnpq)
-  | .XOR_ELIM1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
-    let hpq : Q(XOr $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q($p ∨ $q) q(Prop.xorElim1 $hpq)
-  | .XOR_ELIM2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
-    let hpq : Q(XOr $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$p ∨ ¬$q) q(Prop.xorElim2 $hpq)
-  | .NOT_XOR_ELIM1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]!
-    let hnpq : Q(¬XOr $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q($p ∨ ¬$q) q(Prop.notXorElim1 $hnpq)
-  | .NOT_XOR_ELIM2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getResult[1]!
-    let hnpq : Q(¬XOr $p $q) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$p ∨ $q) q(Prop.notXorElim2 $hnpq)
-  | .NOT_AND =>
-    let fs := pf.getChildren[0]!.getResult[0]!
-    let mut ps : Q(List Prop) := q([])
-    let n := fs.getNumChildren
-    for i in [:n] do
-      let p : Q(Prop) ← reconstructTerm fs[n - i - 1]!
-      ps := q($p :: $ps)
-    let hnps : Q(¬andN $ps) ← reconstructProof pf.getChildren[0]!
-    addThm (← reconstructTerm pf.getResult) (.app q(Prop.notAnd $ps) hnps)
-  | .CNF_AND_POS =>
-    let cnf := pf.getArguments[0]!
-    let i : Nat := pf.getArguments[1]!.getIntegerValue.toNat
-    let mut ps : Q(List Prop) := q([])
-    let n := cnf.getNumChildren
-    for i in [:n] do
-      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
-      ps := q($p :: $ps)
-    addThm (← reconstructTerm pf.getResult) q(Prop.cnfAndPos $ps $i)
-  | .CNF_AND_NEG =>
-    let cnf := pf.getArguments[0]!
-    let mut ps : Q(List Prop) := q([])
-    let n := cnf.getNumChildren
-    for i in [:n] do
-      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
-      ps := q($p :: $ps)
-    addThm (← reconstructTerm pf.getResult) q(Prop.cnfAndNeg $ps)
-  | .CNF_OR_POS =>
-    let cnf := pf.getArguments[0]!
-    let mut ps : Q(List Prop) := q([])
-    let n := cnf.getNumChildren
-    for i in [:n] do
-      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
-      ps := q($p :: $ps)
-    addThm (← reconstructTerm pf.getResult) q(Prop.cnfOrPos $ps)
-  | .CNF_OR_NEG =>
-    let cnf := pf.getArguments[0]!
-    let i : Nat := pf.getArguments[1]!.getIntegerValue.toNat
-    let mut ps : Q(List Prop) := q([])
-    let n := cnf.getNumChildren
-    for i in [:n] do
-      let p : Q(Prop) ← reconstructTerm cnf[n - i - 1]!
-      ps := q($p :: $ps)
-    addThm (← reconstructTerm pf.getResult) q(Prop.cnfOrNeg $ps $i)
-  | .CNF_IMPLIES_POS =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(¬($p → $q) ∨ ¬$p ∨ $q) q(@Prop.cnfImpliesPos $p $q)
-  | .CNF_IMPLIES_NEG1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(($p → $q) ∨ $p) q(@Prop.cnfImpliesNeg1 $p $q)
-  | .CNF_IMPLIES_NEG2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(($p → $q) ∨ ¬$q) q(@Prop.cnfImpliesNeg2 $p $q)
-  | .CNF_EQUIV_POS1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q($p ≠ $q ∨ ¬$p ∨ $q) q(@Prop.cnfEquivPos1 $p $q)
-  | .CNF_EQUIV_POS2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q($p ≠ $q ∨ $p ∨ ¬$q) q(@Prop.cnfEquivPos2 $p $q)
-  | .CNF_EQUIV_NEG1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q($p = $q ∨ $p ∨ $q) q(@Prop.cnfEquivNeg1 $p $q)
-  | .CNF_EQUIV_NEG2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q($p = $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfEquivNeg2 $p $q)
-  | .CNF_XOR_POS1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(¬XOr $p $q ∨ $p ∨ $q) q(@Prop.cnfXorPos1 $p $q)
-  | .CNF_XOR_POS2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(¬XOr $p $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfXorPos2 $p $q)
-  | .CNF_XOR_NEG1 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(XOr $p $q ∨ ¬$p ∨ $q) q(@Prop.cnfXorNeg1 $p $q)
-  | .CNF_XOR_NEG2 =>
-    let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
-    let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]!
-    addThm q(XOr $p $q ∨ $p ∨ ¬$q) q(@Prop.cnfXorNeg2 $p $q)
-  | .TRUE_INTRO =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let hp : Q($p) ← reconstructProof pf.getChildren[0]!
-    addThm q($p = True) q(Prop.trueIntro $hp)
-  | .TRUE_ELIM =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult
-    let hp : Q($p = True) ← reconstructProof pf.getChildren[0]!
-    addThm q($p) q(Prop.trueElim $hp)
-  | .FALSE_INTRO =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let hnp : Q(¬$p) ← reconstructProof pf.getChildren[0]!
-    addThm q($p = False) q(Prop.falseIntro $hnp)
-  | .FALSE_ELIM =>
-    let p : Q(Prop) ← reconstructTerm pf.getResult[0]!
-    let hnp : Q($p = False) ← reconstructProof pf.getChildren[0]!
-    addThm q(¬$p) q(Prop.falseElim $hnp)
-  | _ => return none
-
-end Smt.Reconstruct.Prop
diff --git a/Smt/Reconstruct/Quant.lean b/Smt/Reconstruct/Quant.lean
index 03526f31..e2f43b5a 100644
--- a/Smt/Reconstruct/Quant.lean
+++ b/Smt/Reconstruct/Quant.lean
@@ -5,4 +5,169 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.Quant.Reconstruct
+import Smt.Reconstruct.Quant.Lemmas
+import Smt.Reconstruct
+
+/-- Takes an array `xs` of free variables or metavariables and a term `e` that may contain those variables, and abstracts and binds them as existential quantifiers.
+
+- if `usedOnly = true` then only variables that the expression body depends on will appear.
+- if `usedLetOnly = true` same as `usedOnly` except for let-bound variables. (That is, local constants which have been assigned a value.)
+ -/
+def Lean.Meta.mkExistsFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr := do
+  let e ← if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly binderInfoForMVars
+  addExists e xs.size
+where
+  addExists : Expr → Nat → MetaM Expr
+    | .lam n t b i, m + 1 => do
+      let b ← addExists b m
+      mkAppM ``Exists #[.lam n t b i]
+    | e, _ => pure e
+
+namespace Smt.Reconstruct.Quant
+
+open Lean Qq
+
+@[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with
+  | .FORALL =>
+    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
+    for x in t[0]! do
+      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
+    withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
+      let b ← reconstructTerm t[1]!
+      Meta.mkForallFVars xs b
+  | .EXISTS =>
+    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
+    for x in t[0]! do
+      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
+    withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
+      let b ← reconstructTerm t[1]!
+      Meta.mkExistsFVars xs b
+  | .LAMBDA =>
+    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
+    for x in t[0]! do
+      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
+    withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
+      let b ← reconstructTerm t[1]!
+      Meta.mkLambdaFVars xs b
+  | .HO_APPLY =>
+    return (← reconstructTerm t[0]!).app (← reconstructTerm t[1]!)
+  | .SKOLEM_FUN => match t.getSkolemId with
+    | .QUANTIFIERS_SKOLEMIZE =>
+      let q := t.getSkolemArguments[0]!
+      let n := t.getSkolemArguments[1]!.getIntegerValue.toNat
+      let es ← if q.getKind == .EXISTS then reconstructExistsSkolems q n else reconstructForallSkolems q n
+      return es[n]!
+    | _ => return none
+  | _ => return none
+where
+  reconstructForallSkolems (q : cvc5.Term) (n : Nat) : ReconstructM (Array Expr) := do
+    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
+    let mut es := #[]
+    for x in q[0]![0]! do
+      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
+    let F := q[0]![1]!
+    for i in [0:n + 1] do
+      let α : Q(Type) ← reconstructSort q[0]![0]![i]!.getSort
+      let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
+      let e ← withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
+        let F ← reconstructTerm F
+        let F' := F.replaceFVars xs[0:i] es
+        let ysF' ← Meta.mkExistsFVars xs[i + 1:n + 1] F'
+        let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] (.app q(Not) ysF')
+        return q(@Classical.epsilon $α $h $xysF')
+      es := es.push e
+    return es
+  reconstructExistsSkolems (q : cvc5.Term) (n : Nat) : ReconstructM (Array Expr) := do
+    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
+    let mut es := #[]
+    for x in q[0]! do
+      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
+    let F := q[1]!
+    for i in [0:n + 1] do
+      let α : Q(Type) ← reconstructSort q[0]![i]!.getSort
+      let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
+      let e ← withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
+        let F ← reconstructTerm F
+        let F' := F.replaceFVars xs[0:i] es
+        let ysF' ← Meta.mkExistsFVars xs[i + 1:n + 1] F'
+        let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] ysF'
+        return q(@Classical.epsilon $α $h $xysF')
+      es := es.push e
+    return es
+  getVariableName (t : cvc5.Term) : Name :=
+    if t.hasSymbol then t.getSymbol else Name.num `x t.getId
+  withNewTermCache {α} (k : ReconstructM α) : ReconstructM α := do
+    let state ← get
+    let r ← k
+    set { ← get with termCache := state.termCache }
+    return r
+
+@[smt_proof_reconstruct] def reconstructQuantProof : ProofReconstructor := fun pf => do match pf.getRule with
+  | .CONG =>
+    let k := pf.getResult[0]!.getKind
+    -- This rule needs more care for closures.
+    if k == .FORALL then
+      reconstructForallCong pf
+    else
+      return none
+  | .BETA_REDUCE =>
+    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
+    let t  : Q($α) ← reconstructTerm pf.getResult[0]!
+    let t' : Q($α) ← reconstructTerm pf.getResult[1]!
+    addThm q($t = $t') q(Eq.refl $t)
+  | .SKOLEMIZE => reconstructSkolemize pf
+  | .INSTANTIATE =>
+    let xsF  : Q(Prop) ← reconstructProof pf.getChildren[0]!
+    let mut es := #[]
+    for t in pf.getArguments[0]! do
+      es := es.push (← reconstructTerm t)
+    addThm (← reconstructTerm pf.getResult) (mkAppN xsF es)
+  | .ALPHA_EQUIV =>
+    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
+    let t  : Q($α) ← reconstructTerm pf.getResult[0]!
+    let t' : Q($α) ← reconstructTerm pf.getResult[1]!
+    addThm q($t = $t') q(Eq.refl $t)
+  | _ => return none
+where
+  reconstructForallCong (pf : cvc5.Proof) : ReconstructM Expr := do
+    let mv ← getCurrGoal
+    mv.withContext do
+      let n := reconstructQuant.getVariableName pf.getArguments[1]![0]!
+      let α : Q(Type) ← reconstructSort pf.getArguments[1]![0]!.getSort
+      let mkLam n α t := Meta.withLocalDeclD n α (reconstructTerm t >>= liftM ∘ Meta.mkLambdaFVars #[·])
+      let p : Q($α → Prop) ← mkLam n α pf.getResult[0]![1]!
+      let q : Q($α → Prop) ← mkLam n α pf.getResult[1]![1]!
+      let h : Q(∀ a, $p a = $q a) ← Meta.mkFreshExprMVar q(∀ a, $p a = $q a)
+      let (fv, mv') ← h.mvarId!.intro n
+      let a : Q($α) ← (return .fvar fv)
+      setCurrGoal mv'
+      let h' : Q($p $a = $q $a) ← mv'.withContext (withAssums #[a] (reconstructProof pf.getChildren[0]!))
+      let mv' ← getCurrGoal
+      mv'.withContext (mv'.assignIfDefeq h')
+      setCurrGoal mv
+      addThm q((∀ a, $p a) = (∀ a, $q a)) q(forall_congr $h)
+  reconstructSkolemize (pf : cvc5.Proof) : ReconstructM Expr := do
+    let res := pf.getChildren[0]!.getResult
+    if res.getKind == .EXISTS then
+      let es ← reconstructQuant.reconstructExistsSkolems res (res[0]![0]!.getNumChildren - 1)
+      let f := fun h e => do
+        let α : Q(Type) ← pure (e.getArg! 0)
+        let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
+        let p : Q($α → Prop)  ← pure (e.getArg! 2)
+        let h : Q(∃ x, $p x) ← pure h
+        return q(@Classical.epsilon_spec_aux $α $hα $p $h)
+      let h : Expr ← es.foldlM f (← reconstructProof pf.getChildren[0]!)
+      addThm (← reconstructTerm pf.getResult) h
+    else
+      let es ← reconstructQuant.reconstructForallSkolems res (res[0]![0]!.getNumChildren - 1)
+      let f := fun h e => do
+        let α : Q(Type) ← pure (e.getArg! 0)
+        let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
+        let .lam n _ (.app _ b) bi := e.getArg! 2 | throwError "[skolemize]: expected a predicate with a negated body: {e}"
+        let p : Q($α → Prop)  ← pure (.lam n α b bi)
+        let h : Q(¬∀ x, $p x) ← pure h
+        return q(@Classical.epsilon_spec_aux' $α $hα $p $h)
+      let h : Expr ← es.foldlM f (← reconstructProof pf.getChildren[0]!)
+      addThm (← reconstructTerm pf.getResult) h
+
+end Smt.Reconstruct.Quant
diff --git a/Smt/Reconstruct/Quant/Reconstruct.lean b/Smt/Reconstruct/Quant/Reconstruct.lean
deleted file mode 100644
index 8693d7ac..00000000
--- a/Smt/Reconstruct/Quant/Reconstruct.lean
+++ /dev/null
@@ -1,173 +0,0 @@
-/-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
--/
-
-import Smt.Reconstruct.Quant.Lemmas
-import Smt.Reconstruct.Reconstruct
-
-/-- Takes an array `xs` of free variables or metavariables and a term `e` that may contain those variables, and abstracts and binds them as existential quantifiers.
-
-- if `usedOnly = true` then only variables that the expression body depends on will appear.
-- if `usedLetOnly = true` same as `usedOnly` except for let-bound variables. (That is, local constants which have been assigned a value.)
- -/
-def Lean.Meta.mkExistsFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr := do
-  let e ← if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly binderInfoForMVars
-  addExists e xs.size
-where
-  addExists : Expr → Nat → MetaM Expr
-    | .lam n t b i, m + 1 => do
-      let b ← addExists b m
-      mkAppM ``Exists #[.lam n t b i]
-    | e, _ => pure e
-
-namespace Smt.Reconstruct.Quant
-
-open Lean Qq
-
-@[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with
-  | .FORALL =>
-    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
-    for x in t[0]! do
-      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
-    withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
-      let b ← reconstructTerm t[1]!
-      Meta.mkForallFVars xs b
-  | .EXISTS =>
-    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
-    for x in t[0]! do
-      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
-    withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
-      let b ← reconstructTerm t[1]!
-      Meta.mkExistsFVars xs b
-  | .LAMBDA =>
-    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
-    for x in t[0]! do
-      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
-    withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
-      let b ← reconstructTerm t[1]!
-      Meta.mkLambdaFVars xs b
-  | .HO_APPLY =>
-    return (← reconstructTerm t[0]!).app (← reconstructTerm t[1]!)
-  | .SKOLEM_FUN => match t.getSkolemId with
-    | .QUANTIFIERS_SKOLEMIZE =>
-      let q := t.getSkolemArguments[0]!
-      let n := t.getSkolemArguments[1]!.getIntegerValue.toNat
-      let es ← if q.getKind == .EXISTS then reconstructExistsSkolems q n else reconstructForallSkolems q n
-      return es[n]!
-    | _ => return none
-  | _ => return none
-where
-  reconstructForallSkolems (q : cvc5.Term) (n : Nat) : ReconstructM (Array Expr) := do
-    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
-    let mut es := #[]
-    for x in q[0]![0]! do
-      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
-    let F := q[0]![1]!
-    for i in [0:n + 1] do
-      let α : Q(Type) ← reconstructSort q[0]![0]![i]!.getSort
-      let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
-      let e ← withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
-        let F ← reconstructTerm F
-        let F' := F.replaceFVars xs[0:i] es
-        let ysF' ← Meta.mkExistsFVars xs[i + 1:n + 1] F'
-        let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] (.app q(Not) ysF')
-        return q(@Classical.epsilon $α $h $xysF')
-      es := es.push e
-    return es
-  reconstructExistsSkolems (q : cvc5.Term) (n : Nat) : ReconstructM (Array Expr) := do
-    let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[]
-    let mut es := #[]
-    for x in q[0]! do
-      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
-    let F := q[1]!
-    for i in [0:n + 1] do
-      let α : Q(Type) ← reconstructSort q[0]![i]!.getSort
-      let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
-      let e ← withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do
-        let F ← reconstructTerm F
-        let F' := F.replaceFVars xs[0:i] es
-        let ysF' ← Meta.mkExistsFVars xs[i + 1:n + 1] F'
-        let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] ysF'
-        return q(@Classical.epsilon $α $h $xysF')
-      es := es.push e
-    return es
-  getVariableName (t : cvc5.Term) : Name :=
-    if t.hasSymbol then t.getSymbol else Name.num `x t.getId
-  withNewTermCache {α} (k : ReconstructM α) : ReconstructM α := do
-    let state ← get
-    let r ← k
-    set { ← get with termCache := state.termCache }
-    return r
-
-@[smt_proof_reconstruct] def reconstructQuantProof : ProofReconstructor := fun pf => do match pf.getRule with
-  | .CONG =>
-    let k := pf.getResult[0]!.getKind
-    -- This rule needs more care for closures.
-    if k == .FORALL then
-      reconstructForallCong pf
-    else
-      return none
-  | .BETA_REDUCE =>
-    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
-    let t  : Q($α) ← reconstructTerm pf.getResult[0]!
-    let t' : Q($α) ← reconstructTerm pf.getResult[1]!
-    addThm q($t = $t') q(Eq.refl $t)
-  | .SKOLEMIZE => reconstructSkolemize pf
-  | .INSTANTIATE =>
-    let xsF  : Q(Prop) ← reconstructProof pf.getChildren[0]!
-    let mut es := #[]
-    for t in pf.getArguments[0]! do
-      es := es.push (← reconstructTerm t)
-    addThm (← reconstructTerm pf.getResult) (mkAppN xsF es)
-  | .ALPHA_EQUIV =>
-    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
-    let t  : Q($α) ← reconstructTerm pf.getResult[0]!
-    let t' : Q($α) ← reconstructTerm pf.getResult[1]!
-    addThm q($t = $t') q(Eq.refl $t)
-  | _ => return none
-where
-  reconstructForallCong (pf : cvc5.Proof) : ReconstructM Expr := do
-    let mv ← getCurrGoal
-    mv.withContext do
-      let n := reconstructQuant.getVariableName pf.getArguments[1]![0]!
-      let α : Q(Type) ← reconstructSort pf.getArguments[1]![0]!.getSort
-      let mkLam n α t := Meta.withLocalDeclD n α (reconstructTerm t >>= liftM ∘ Meta.mkLambdaFVars #[·])
-      let p : Q($α → Prop) ← mkLam n α pf.getResult[0]![1]!
-      let q : Q($α → Prop) ← mkLam n α pf.getResult[1]![1]!
-      let h : Q(∀ a, $p a = $q a) ← Meta.mkFreshExprMVar q(∀ a, $p a = $q a)
-      let (fv, mv') ← h.mvarId!.intro n
-      let a : Q($α) ← (return .fvar fv)
-      setCurrGoal mv'
-      let h' : Q($p $a = $q $a) ← mv'.withContext (withAssums #[a] (reconstructProof pf.getChildren[0]!))
-      let mv' ← getCurrGoal
-      mv'.withContext (mv'.assignIfDefeq h')
-      setCurrGoal mv
-      addThm q((∀ a, $p a) = (∀ a, $q a)) q(forall_congr $h)
-  reconstructSkolemize (pf : cvc5.Proof) : ReconstructM Expr := do
-    let res := pf.getChildren[0]!.getResult
-    if res.getKind == .EXISTS then
-      let es ← reconstructQuant.reconstructExistsSkolems res (res[0]![0]!.getNumChildren - 1)
-      let f := fun h e => do
-        let α : Q(Type) ← pure (e.getArg! 0)
-        let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
-        let p : Q($α → Prop)  ← pure (e.getArg! 2)
-        let h : Q(∃ x, $p x) ← pure h
-        return q(@Classical.epsilon_spec_aux $α $hα $p $h)
-      let h : Expr ← es.foldlM f (← reconstructProof pf.getChildren[0]!)
-      addThm (← reconstructTerm pf.getResult) h
-    else
-      let es ← reconstructQuant.reconstructForallSkolems res (res[0]![0]!.getNumChildren - 1)
-      let f := fun h e => do
-        let α : Q(Type) ← pure (e.getArg! 0)
-        let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
-        let .lam n _ (.app _ b) bi := e.getArg! 2 | throwError "[skolemize]: expected a predicate with a negated body: {e}"
-        let p : Q($α → Prop)  ← pure (.lam n α b bi)
-        let h : Q(¬∀ x, $p x) ← pure h
-        return q(@Classical.epsilon_spec_aux' $α $hα $p $h)
-      let h : Expr ← es.foldlM f (← reconstructProof pf.getChildren[0]!)
-      addThm (← reconstructTerm pf.getResult) h
-
-end Smt.Reconstruct.Quant
diff --git a/Smt/Reconstruct/Reconstruct.lean b/Smt/Reconstruct/Reconstruct.lean
deleted file mode 100644
index 348da56b..00000000
--- a/Smt/Reconstruct/Reconstruct.lean
+++ /dev/null
@@ -1,217 +0,0 @@
-import cvc5
-import Qq
-import Std
-
-import Smt.Attribute
-
-namespace Smt
-
-open Lean
-open Attribute
-
-structure Reconstruct.state where
-  termCache : HashMap cvc5.Term Expr
-  proofCache : HashMap cvc5.Proof Expr
-  count : Nat
-  trusts : Array cvc5.Proof
-  mainGoal : MVarId
-  currGoal : MVarId
-  currAssums : Array Expr
-  skipedGoals : Array MVarId
-
-abbrev ReconstructM := StateT Reconstruct.state MetaM
-
-abbrev SortReconstructor := cvc5.Sort → ReconstructM (Option Expr)
-
-abbrev TermReconstructor := cvc5.Term → ReconstructM (Option Expr)
-
-abbrev ProofReconstructor := cvc5.Proof → ReconstructM (Option Expr)
-
-namespace Reconstruct
-
-private unsafe def getReconstructorsUnsafe (n : Name) (rcons : Type) : MetaM (List (rcons × Name)) := do
-  let env ← getEnv
-  let names := ((smtExt.getState env).findD n {}).toList
-  let mut reconstructors := []
-  for name in names do
-    let fn ← IO.ofExcept <| Id.run <| ExceptT.run <|
-      env.evalConst rcons Options.empty name
-    reconstructors := (fn, name) :: reconstructors
-  return reconstructors
-
-@[implemented_by getReconstructorsUnsafe]
-opaque getReconstructors (n : Name) (rcons : Type) : MetaM (List (rcons × Name))
-
-def reconstructSort (s : cvc5.Sort) : ReconstructM Expr := do
-  let rs ← getReconstructors ``SortReconstructor SortReconstructor
-  go rs s
-where
-  go (rs : List (SortReconstructor × Name)) (s : cvc5.Sort) : ReconstructM Expr := do
-    for (r, n) in rs do
-      if let some e ← r s then
-        trace[smt.debug.reconstruct.sort] "{s} =({n})=> {e}"
-        return e
-    throwError "Failed to reconstruct sort {s} with kind {repr s.getKind}"
-
-def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : ReconstructM MessageData :=
-  return m!"{t} ↦ " ++ match r with
-    | .ok e    => m!"{e}"
-    | .error _ => m!"{bombEmoji}"
-
-def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t =>
-  withTraceNode `smt.debug.reconstruct (traceReconstructTerm t) do
-    let rs ← getReconstructors ``TermReconstructor TermReconstructor
-    go rs t
-where
-  withTermCache (r : cvc5.Term → ReconstructM Expr) (t : cvc5.Term) : ReconstructM Expr := do
-    match (← get).termCache.find? t with
-    -- TODO: cvc5's global bound variables mess up the cache. Find a fix.
-    | some e => if e.hasFVar then reconstruct r t else return e
-    | none   => reconstruct r t
-  reconstruct r t := do
-    let e ← r t
-    modify fun state => { state with termCache := state.termCache.insert t e }
-    return e
-  go (rs : List (TermReconstructor × Name)) (t : cvc5.Term) : ReconstructM Expr := do
-    for (r, n) in rs do
-      if let some e ← r t then
-        trace[smt.debug.reconstruct.term] "{t} =({n})=> {e}"
-        return e
-    throwError "Failed to reconstruct term {t} with kind {repr t.getKind}"
-
-def withProofCache (r : cvc5.Proof → ReconstructM Expr) (p : cvc5.Proof) : ReconstructM Expr := do
-  match (← get).proofCache.find? p with
-  | some e => (← get).currGoal.withContext do
-    if (← getLCtx).containsFVar e then return e else reconstruct r p
-  | none   => reconstruct r p
-where
-  reconstruct r p := do
-    let e ← r p
-    modify fun state => { state with proofCache := state.proofCache.insert p e }
-    return e
-
-def incCount : ReconstructM Nat :=
-  modifyGet fun state => (state.count, { state with count := state.count + 1 })
-
-def withAssums (as : Array Expr) (k : ReconstructM α) : ReconstructM α := do
-  modify fun state => { state with currAssums := state.currAssums ++ as }
-  let r ← k
-  modify fun state => { state with currAssums := state.currAssums.shrink (state.currAssums.size - as.size) }
-  return r
-
-def skipStep (mv : MVarId) : ReconstructM Unit := mv.withContext do
-  let state ← get
-  let t ← Meta.mkForallFVars state.currAssums (← mv.getType)
-  let mv' ← state.mainGoal.withContext (Meta.mkFreshExprMVar t)
-  let e := mkAppN mv' state.currAssums
-  set { state with skipedGoals := state.skipedGoals.push mv'.mvarId! }
-  mv.assignIfDefeq e
-
-def getCurrGoal : ReconstructM MVarId :=
-  get >>= (pure ·.currGoal)
-
-def setCurrGoal (mv : MVarId) : ReconstructM Unit :=
-  modify fun state => { state with currGoal := mv }
-
-def addThm (type : Expr) (val : Expr) : ReconstructM Expr := do
-  let mv ← getCurrGoal
-  mv.withContext do
-    let name := Name.num `s (← incCount)
-    let (fv, mv) ← (← mv.assert name type val).intro1P
-    trace[smt.debug.reconstruct.proof] "have {name} : {type} := {val}"
-    setCurrGoal mv
-    return .fvar fv
-
-def addTac (type : Expr) (tac : MVarId → MetaM Unit) : ReconstructM Expr := do
-  let mv ← getCurrGoal
-  mv.withContext do
-    let name := Name.num `s (← incCount)
-    let mv' ← Meta.mkFreshExprMVar type
-    tac mv'.mvarId!
-    let (fv, mv) ← (← mv.assert name type mv').intro1P
-    trace[smt.debug.reconstruct.proof] "have {name} : {type} := by {mv'}"
-    setCurrGoal mv
-    return .fvar fv
-
-def addTrust (type : Expr) (pf : cvc5.Proof) : ReconstructM Expr := do
-  let mv ← getCurrGoal
-  mv.withContext do
-    let name := Name.num `s (← incCount)
-    let mv' ← Meta.mkFreshExprMVar type
-    skipStep mv'.mvarId!
-    let (fv, mv) ← (← mv.assert name type mv').intro1P
-    trace[smt.debug.reconstruct.proof] m!"have {name} : {type} := sorry"
-    trace[smt.debug.reconstruct.proof]
-      m!"rule : {repr pf.getRule}\npremises : {pf.getChildren.map (·.getResult)}\nargs : {pf.getArguments}\nconclusion : {pf.getResult}"
-    modify fun state => { state with trusts := state.trusts.push pf }
-    setCurrGoal mv
-    return .fvar fv
-
-partial def reconstructProof : cvc5.Proof → ReconstructM Expr := withProofCache fun pf => do
-  let rs ← getReconstructors ``ProofReconstructor ProofReconstructor
-  go rs pf
-where
-  go (rs : List (ProofReconstructor × Name)) (pf : cvc5.Proof) : ReconstructM Expr := do
-    for (r, _) in rs do
-      if let some e ← r pf then
-        return e
-    _ ← pf.getChildren.mapM reconstructProof
-    let type ← reconstructTerm pf.getResult
-    addTrust type pf
-
-end Reconstruct
-
-def traceReconstructProof (r : Except Exception (FVarId × MVarId × List MVarId)) : MetaM MessageData :=
-  return match r with
-  | .ok _ => m!"{checkEmoji}"
-  | _     => m!"{bombEmoji}"
-
-open Qq in
-partial def reconstructProof (mv : MVarId) (pf : cvc5.Proof) : MetaM (FVarId × MVarId × List MVarId) :=
-  withTraceNode `smt.debug.reconstruct traceReconstructProof do
-  let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨{}, {}, 0, #[], mv, mv, #[], #[]⟩
-  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mv _ mvs) ← (Reconstruct.reconstructProof pf).run state
-  let ⟨fv, mv, _⟩ ← mv.replace h.fvarId! q($h trivial) q($p)
-  return (fv, mv, mvs.toList)
-
-open cvc5 in
-def traceProve (r : Except Exception (Except SolverError Proof)) : MetaM MessageData :=
-  return match r with
-  | .ok (.ok _) => m!"{checkEmoji}"
-  | _           => m!"{bombEmoji}"
-
-open cvc5 in
-def prove (query : String) (timeout : Option Nat) : MetaM (Except SolverError cvc5.Proof) :=
-  withTraceNode `smt.debug.prove traceProve do Solver.run do
-    if let .some timeout := timeout then
-      Solver.setOption "tlimit" (toString (1000*timeout))
-    Solver.setOption "dag-thresh" "0"
-    Solver.setOption "simplification" "none"
-    Solver.setOption "enum-inst" "true"
-    Solver.setOption "produce-models" "true"
-    Solver.setOption "produce-proofs" "true"
-    Solver.setOption "proof-elim-subtypes" "true"
-    Solver.setOption "proof-granularity" "dsl-rewrite"
-    Solver.parse query
-    let r ← Solver.checkSat
-    if r.isUnsat then
-      let ps ← Solver.getProof
-      if h : 0 < ps.size then
-        trace[smt.debug.reconstruct] (← Solver.proofToString ps[0])
-        return ps[0]
-    throw (self := instMonadExcept _ _) (SolverError.user_error "something went wrong")
-
-syntax (name := reconstruct) "reconstruct" str : tactic
-
-open Lean.Elab Tactic in
-@[tactic reconstruct] def evalReconstruct : Tactic := fun stx =>
-  withMainContext do
-    let some query := stx[1].isStrLit? | throwError "expected string"
-    let r ← prove query none
-    match r with
-      | .error e => logInfo (repr e)
-      | .ok pf =>
-        let (_, mv, mvs) ← reconstructProof (← getMainGoal) pf
-        replaceMainGoal (mv :: mvs)
-
-end Smt
diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean
index 03781b3f..3aeca1b3 100644
--- a/Smt/Reconstruct/UF.lean
+++ b/Smt/Reconstruct/UF.lean
@@ -5,4 +5,99 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.UF.Reconstruct
+import Smt.Reconstruct
+import Smt.Reconstruct.UF.Congruence
+import Smt.Reconstruct.UF.Rewrites
+
+namespace Smt.Reconstruct.UF
+
+open Lean Qq
+
+def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
+  match (← getLCtx).findFromUserName? n with
+  | some d => return d.toExpr
+  | none   =>
+    let c ← getConstInfo n
+    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+
+@[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with
+  | .INTERNAL_SORT_KIND
+  | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol
+  | _             => return none
+
+@[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
+  | .EQUAL =>
+    let α : Q(Type) ← reconstructSort t[0]!.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x = $y)
+  | .DISTINCT =>
+    let α : Q(Type) ← reconstructSort t[0]!.getSort
+    let x : Q($α) ← reconstructTerm t[0]!
+    let y : Q($α) ← reconstructTerm t[1]!
+    return q($x ≠ $y)
+  | .APPLY_UF =>
+    let mut curr ← reconstructTerm t[0]!
+    for i in [1:t.getNumChildren] do
+      curr := .app curr (← reconstructTerm t[i]!)
+    return curr
+  | _ => return none
+
+def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
+  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
+  | .EQ_REFL =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
+    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
+    addThm q(($t = $t) = True) q(@UF.eq_refl $α $t)
+  | .EQ_SYMM =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
+    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
+    let s : Q($α) ← reconstructTerm pf.getArguments[2]!
+    addThm q(($t = $s) = ($s = $t)) q(@UF.eq_symm $α $t $s)
+  | .DISTINCT_BINARY_ELIM =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
+    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
+    let s : Q($α) ← reconstructTerm pf.getArguments[2]!
+    addThm q(($t ≠ $s) = ¬($t = $s)) q(@UF.distinct_binary_elim $α $t $s)
+  | _ => return none
+
+@[smt_proof_reconstruct] def reconstructUFProof : ProofReconstructor := fun pf => do match pf.getRule with
+  | .DSL_REWRITE => reconstructRewrite pf
+  | .REFL =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[0]!.getSort
+    let a : Q($α) ← reconstructTerm pf.getArguments[0]!
+    addThm q($a = $a) q(Eq.refl $a)
+  | .SYMM =>
+    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
+    let a : Q($α) ← reconstructTerm pf.getResult[1]!
+    let b : Q($α) ← reconstructTerm pf.getResult[0]!
+    if pf.getResult.getKind == .EQUAL then
+      let h : Q($a = $b) ← reconstructProof pf.getChildren[0]!
+      addThm q($b = $a) q(Eq.symm $h)
+    else
+      let h : Q($a ≠ $b) ← reconstructProof pf.getChildren[0]!
+      addThm q($b ≠ $a) q(Ne.symm $h)
+  | .TRANS =>
+    let cpfs := pf.getChildren
+    let α : Q(Type) ← reconstructSort cpfs[0]!.getResult[0]!.getSort
+    let a : Q($α) ← reconstructTerm cpfs[0]!.getResult[0]!
+    let mut curr ← reconstructProof cpfs[0]!
+    for i in [1:cpfs.size] do
+      let b : Q($α) ← reconstructTerm cpfs[i]!.getResult[0]!
+      let c : Q($α) ← reconstructTerm cpfs[i]!.getResult[1]!
+      let hab : Q($a = $b) := curr
+      let hbc : Q($b = $c) ← reconstructProof cpfs[i]!
+      curr ← addThm q($a = $c) q(Eq.trans $hab $hbc)
+    return curr
+  | .CONG =>
+    let k := pf.getResult[0]!.getKind
+    if k == .FORALL || k == .EXISTS || k == .WITNESS || k == .LAMBDA || k == .SET_COMPREHENSION then
+      return none
+    let mut assums ← pf.getChildren.mapM reconstructProof
+    addTac (← reconstructTerm pf.getResult) (smtCongr · assums)
+  | .NARY_CONG =>
+    let mut assums ← pf.getChildren.mapM reconstructProof
+    addTac (← reconstructTerm pf.getResult) (smtCongr · assums)
+  | _ => return none
+
+end Smt.Reconstruct.UF
diff --git a/Smt/Reconstruct/UF/Reconstruct.lean b/Smt/Reconstruct/UF/Reconstruct.lean
deleted file mode 100644
index 9832f575..00000000
--- a/Smt/Reconstruct/UF/Reconstruct.lean
+++ /dev/null
@@ -1,103 +0,0 @@
-/-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
--/
-
-import Smt.Reconstruct.Reconstruct
-import Smt.Reconstruct.UF.Congruence
-import Smt.Reconstruct.UF.Rewrites
-
-namespace Smt.Reconstruct.UF
-
-open Lean Qq
-
-def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   =>
-    let c ← getConstInfo n
-    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
-
-@[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with
-  | .INTERNAL_SORT_KIND
-  | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol
-  | _             => return none
-
-@[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
-  | .EQUAL =>
-    let α : Q(Type) ← reconstructSort t[0]!.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x = $y)
-  | .DISTINCT =>
-    let α : Q(Type) ← reconstructSort t[0]!.getSort
-    let x : Q($α) ← reconstructTerm t[0]!
-    let y : Q($α) ← reconstructTerm t[1]!
-    return q($x ≠ $y)
-  | .APPLY_UF =>
-    let mut curr ← reconstructTerm t[0]!
-    for i in [1:t.getNumChildren] do
-      curr := .app curr (← reconstructTerm t[i]!)
-    return curr
-  | _ => return none
-
-def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with
-  | .EQ_REFL =>
-    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
-    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
-    addThm q(($t = $t) = True) q(@UF.eq_refl $α $t)
-  | .EQ_SYMM =>
-    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
-    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
-    let s : Q($α) ← reconstructTerm pf.getArguments[2]!
-    addThm q(($t = $s) = ($s = $t)) q(@UF.eq_symm $α $t $s)
-  | .DISTINCT_BINARY_ELIM =>
-    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
-    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
-    let s : Q($α) ← reconstructTerm pf.getArguments[2]!
-    addThm q(($t ≠ $s) = ¬($t = $s)) q(@UF.distinct_binary_elim $α $t $s)
-  | _ => return none
-
-@[smt_proof_reconstruct] def reconstructUFProof : ProofReconstructor := fun pf => do match pf.getRule with
-  | .DSL_REWRITE => reconstructRewrite pf
-  | .REFL =>
-    let α : Q(Type) ← reconstructSort pf.getArguments[0]!.getSort
-    let a : Q($α) ← reconstructTerm pf.getArguments[0]!
-    addThm q($a = $a) q(Eq.refl $a)
-  | .SYMM =>
-    let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
-    let a : Q($α) ← reconstructTerm pf.getResult[1]!
-    let b : Q($α) ← reconstructTerm pf.getResult[0]!
-    if pf.getResult.getKind == .EQUAL then
-      let h : Q($a = $b) ← reconstructProof pf.getChildren[0]!
-      addThm q($b = $a) q(Eq.symm $h)
-    else
-      let h : Q($a ≠ $b) ← reconstructProof pf.getChildren[0]!
-      addThm q($b ≠ $a) q(Ne.symm $h)
-  | .TRANS =>
-    let cpfs := pf.getChildren
-    let α : Q(Type) ← reconstructSort cpfs[0]!.getResult[0]!.getSort
-    let a : Q($α) ← reconstructTerm cpfs[0]!.getResult[0]!
-    let mut curr ← reconstructProof cpfs[0]!
-    for i in [1:cpfs.size] do
-      let b : Q($α) ← reconstructTerm cpfs[i]!.getResult[0]!
-      let c : Q($α) ← reconstructTerm cpfs[i]!.getResult[1]!
-      let hab : Q($a = $b) := curr
-      let hbc : Q($b = $c) ← reconstructProof cpfs[i]!
-      curr ← addThm q($a = $c) q(Eq.trans $hab $hbc)
-    return curr
-  | .CONG =>
-    let k := pf.getResult[0]!.getKind
-    if k == .FORALL || k == .EXISTS || k == .WITNESS || k == .LAMBDA || k == .SET_COMPREHENSION then
-      return none
-    let mut assums ← pf.getChildren.mapM reconstructProof
-    addTac (← reconstructTerm pf.getResult) (smtCongr · assums)
-  | .NARY_CONG =>
-    let mut assums ← pf.getChildren.mapM reconstructProof
-    addTac (← reconstructTerm pf.getResult) (smtCongr · assums)
-  | _ => return none
-
-end Smt.Reconstruct.UF
diff --git a/Smt/String.lean b/Smt/String.lean
new file mode 100644
index 00000000..8cabaafa
--- /dev/null
+++ b/Smt/String.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Translate.String
diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean
index bf098d22..bc62950a 100644
--- a/Smt/Tactic/Smt.lean
+++ b/Smt/Tactic/Smt.lean
@@ -8,8 +8,8 @@ Authors: Abdalrhman Mohamed
 import Lean
 
 import Smt.Dsl.Sexp
+import Smt.Reconstruct
 import Smt.Reconstruct.Prop.Lemmas
-import Smt.Reconstruct.Reconstruct
 import Smt.Translate.Query
 import Smt.Util
 
@@ -17,7 +17,7 @@ namespace Smt
 
 open Lean hiding Command
 open Elab Tactic Qq
-open Smt Reconstruct Translate Query
+open Smt Translate Query Reconstruct Util
 
 initialize
   registerTraceClass `smt.debug
diff --git a/Smt/Translate.lean b/Smt/Translate.lean
index fee497f3..c14e0441 100644
--- a/Smt/Translate.lean
+++ b/Smt/Translate.lean
@@ -1,19 +1,138 @@
 /-
-Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+Copyright (c) 2021-2022 by the authors listed in the file AUTHORS and their
 institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
+Authors: Abdalrhman Mohamed, Wojciech Nawrocki
 -/
 
-import Smt.Translate.BitVec
-import Smt.Translate.Bool
-import Smt.Translate.Commands
-import Smt.Translate.Int
-import Smt.Translate.Nat
-import Smt.Translate.Prop
-import Smt.Translate.Query
-import Smt.Translate.Real
-import Smt.Translate.Solver
-import Smt.Translate.String
+import Lean
+
+import Smt.Attribute
 import Smt.Translate.Term
-import Smt.Translate.Translator
+import Smt.Util
+
+namespace Smt
+
+open Lean Meta Expr
+open Attribute Term
+
+structure TranslationM.State where
+  /-- Constants that the translated result depends on. We propagate these upwards during translation
+  in order to build a dependency graph. The value is reset at the `translateExpr` entry point. -/
+  depConstants : NameSet := .empty
+  /-- Memoizes `applyTranslators?` calls together with what they add to `depConstants`. -/
+  cache : HashMap Expr (Option (Term × NameSet)) := .empty
+
+abbrev TranslationM := StateT TranslationM.State MetaM
+
+/-- A function which translates some subset of Lean expressions to SMT-LIBv2 `Term`s. We use
+the combination of all registered translators to encode a fragment of Lean into the many-sorted
+first-order logic of SMT-LIBv2. New translators can be registered with the `smt_translate` attribute.
+
+The input expression is guaranteed to be well-typed in the `MetaM` context. The return value is:
+- `some t` when the translator supports the input and translates it to `t`
+- `none` when the translator doesn't support the input -/
+abbrev Translator := Expr → TranslationM (Option Term)
+
+namespace Translator
+
+private unsafe def getTranslatorsUnsafe : MetaM (List (Translator × Name)) := do
+  let env ← getEnv
+  let names := ((smtExt.getState env).findD ``Translator {}).toList
+  -- trace[smt.debug.attr] "Translators: {names}"
+  let mut translators := []
+  for name in names do
+    let fn ← IO.ofExcept <| Id.run <| ExceptT.run <|
+      env.evalConst Translator Options.empty name
+    translators := (fn, name) :: translators
+  return translators
+
+/-- Returns the list of translators maintained by `smtExt` in the current
+    Lean environment. -/
+@[implemented_by getTranslatorsUnsafe]
+opaque getTranslators : MetaM (List (Translator × Name))
+
+/-- Return a cached translation of `e` if found, otherwise run `k e` and cache the result. -/
+def withCache (k : Translator) (e : Expr) : TranslationM (Option Term) := do
+  match (← get).cache.find? e with
+  | some (some (tm, deps)) =>
+    modify fun st => { st with depConstants := st.depConstants.union deps }
+    return some tm
+  | some none =>
+    return none
+  | none =>
+    let depConstantsBefore := (← get).depConstants
+    modify fun st => { st with depConstants := .empty }
+    let ret? ← k e
+    modify fun st => { st with
+      depConstants := st.depConstants.union depConstantsBefore
+      cache := st.cache.insert e <| ret?.map ((·, st.depConstants))
+    }
+    return ret?
+
+mutual
+
+/-- Like `applyTranslators?` but must succeed. -/
+partial def applyTranslators! (e : Expr) : TranslationM Term := do
+  let some tm ← applyTranslators? e | throwError "no translator matched {e}"
+  return tm
+
+/-- Traverses `e` to compute its SMT-LIB translation. First all translators are tried on the whole
+expression and if one succeeds, its result is returned. Otherwise, `e` is split into subexpressions
+which are then recursively translated and put together into an SMT-LIB term. The traversal proceeds
+in a top-down, depth-first order. -/
+partial def applyTranslators? : Translator := withCache fun e => do
+  let ts ← getTranslators
+  go ts e
+  where
+    go (ts : List (Translator × Name)) : Translator := fun e => do
+      -- First try all translators on the whole expression
+      -- TODO: Use `DiscrTree` to index the translators instead of naively looping
+      for (t, nm) in ts do
+        if let some tm ← t e then
+          trace[smt.debug.translate.expr] "{e} =({nm})=> {tm}"
+          return tm
+
+      -- Then try splitting subexpressions
+      match e with
+      | fvar fv =>
+        let ld ← fv.getDecl
+        return symbolT ld.userName.toString
+      | const nm _ =>
+        modify fun st => { st with depConstants := st.depConstants.insert nm }
+        return symbolT nm.toString
+      | app f e => return appT (← applyTranslators! f) (← applyTranslators! e)
+      | lam .. => throwError "cannot translate {e}, SMT-LIB does not support lambdas"
+      | forallE n t b bi =>
+        let tmB ← Meta.withLocalDecl n bi t (fun x => applyTranslators! <| b.instantiate #[x])
+        if !b.hasLooseBVars /- not a dependent arrow -/ then
+          return arrowT (← applyTranslators! t) tmB
+        else
+          return forallT n.toString (← applyTranslators! t) tmB
+      | letE n t v b _ =>
+        let tmB ← Meta.withLetDecl n t v (fun x => applyTranslators! <| b.instantiate #[x])
+        return letT n.toString (← applyTranslators! v) tmB
+      | mdata _ e => go ts e
+      | e         => throwError "cannot translate {e}"
+
+end
+
+def traceTranslation (e : Expr) (e' : Except ε (Term × NameSet)) : TranslationM MessageData :=
+  return m!"{e} ↦ " ++ match e' with
+    | .ok (e', _) => m!"{e'}"
+    | .error _    => m!"{bombEmoji}"
+
+/-- Processes `e` by running it through all the registered `Translator`s.
+Returns the resulting SMT-LIB term and set of dependencies. -/
+def translateExpr (e : Expr) : TranslationM (Term × NameSet) :=
+  withTraceNode `smt.debug.translate (traceTranslation e ·) do
+    modify fun st => { st with depConstants := .empty }
+    trace[smt.debug.translate.expr] "before: {e}"
+    let tm ← applyTranslators! e
+    trace[smt.debug.translate.expr] "translated: {tm}"
+    return (tm, (← get).depConstants)
+
+def translateExpr' (e : Expr) : TranslationM Term :=
+  Prod.fst <$> translateExpr e
+
+end Smt.Translator
diff --git a/Smt/Translate/BitVec.lean b/Smt/Translate/BitVec.lean
index 80d966e3..2286010a 100644
--- a/Smt/Translate/BitVec.lean
+++ b/Smt/Translate/BitVec.lean
@@ -9,7 +9,7 @@ import Lean
 import Qq
 import Std
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.BitVec
 
diff --git a/Smt/Translate/Bool.lean b/Smt/Translate/Bool.lean
index 49691c3a..96eb517a 100644
--- a/Smt/Translate/Bool.lean
+++ b/Smt/Translate/Bool.lean
@@ -8,7 +8,7 @@ Authors: Abdalrhman Mohamed, Wojciech Nawrocki
 import Lean
 import Qq
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.Bool
 
diff --git a/Smt/Translate/Int.lean b/Smt/Translate/Int.lean
index 3adc0f99..3f9c9d5d 100644
--- a/Smt/Translate/Int.lean
+++ b/Smt/Translate/Int.lean
@@ -9,7 +9,7 @@ import Lean
 import Qq
 import Std
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.Int
 
diff --git a/Smt/Translate/Nat.lean b/Smt/Translate/Nat.lean
index 35952972..12a32561 100644
--- a/Smt/Translate/Nat.lean
+++ b/Smt/Translate/Nat.lean
@@ -8,7 +8,7 @@ Authors: Abdalrhman Mohamed, Wojciech Nawrocki
 import Lean
 import Qq
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.Nat
 
diff --git a/Smt/Translate/Prop.lean b/Smt/Translate/Prop.lean
index e942cb8a..c3686bfb 100644
--- a/Smt/Translate/Prop.lean
+++ b/Smt/Translate/Prop.lean
@@ -8,7 +8,7 @@ Authors: Abdalrhman Mohamed, Wojciech Nawrocki
 import Lean
 import Qq
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.Prop
 
diff --git a/Smt/Translate/Query.lean b/Smt/Translate/Query.lean
index 8851947a..d7500505 100644
--- a/Smt/Translate/Query.lean
+++ b/Smt/Translate/Query.lean
@@ -9,7 +9,7 @@ import Lean
 
 import Smt.Data.Graph
 import Smt.Translate.Commands
-import Smt.Translate.Translator
+import Smt.Translate
 import Smt.Tactic.EqnDef
 import Smt.Util
 
diff --git a/Smt/Translate/Real.lean b/Smt/Translate/Real.lean
index 31dcb59f..3686e9cc 100644
--- a/Smt/Translate/Real.lean
+++ b/Smt/Translate/Real.lean
@@ -10,7 +10,7 @@ import Qq
 
 import Mathlib.Data.Real.Archimedean
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.Rat
 
diff --git a/Smt/Translate/String.lean b/Smt/Translate/String.lean
index 8e9b9f98..7127687a 100644
--- a/Smt/Translate/String.lean
+++ b/Smt/Translate/String.lean
@@ -8,7 +8,7 @@ Authors: Abdalrhman Mohamed, Wojciech Nawrocki
 import Lean
 import Qq
 
-import Smt.Translate.Translator
+import Smt.Translate
 
 namespace Smt.Translate.String
 
diff --git a/Smt/Translate/Translator.lean b/Smt/Translate/Translator.lean
deleted file mode 100644
index c14e0441..00000000
--- a/Smt/Translate/Translator.lean
+++ /dev/null
@@ -1,138 +0,0 @@
-/-
-Copyright (c) 2021-2022 by the authors listed in the file AUTHORS and their
-institutional affiliations. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed, Wojciech Nawrocki
--/
-
-import Lean
-
-import Smt.Attribute
-import Smt.Translate.Term
-import Smt.Util
-
-namespace Smt
-
-open Lean Meta Expr
-open Attribute Term
-
-structure TranslationM.State where
-  /-- Constants that the translated result depends on. We propagate these upwards during translation
-  in order to build a dependency graph. The value is reset at the `translateExpr` entry point. -/
-  depConstants : NameSet := .empty
-  /-- Memoizes `applyTranslators?` calls together with what they add to `depConstants`. -/
-  cache : HashMap Expr (Option (Term × NameSet)) := .empty
-
-abbrev TranslationM := StateT TranslationM.State MetaM
-
-/-- A function which translates some subset of Lean expressions to SMT-LIBv2 `Term`s. We use
-the combination of all registered translators to encode a fragment of Lean into the many-sorted
-first-order logic of SMT-LIBv2. New translators can be registered with the `smt_translate` attribute.
-
-The input expression is guaranteed to be well-typed in the `MetaM` context. The return value is:
-- `some t` when the translator supports the input and translates it to `t`
-- `none` when the translator doesn't support the input -/
-abbrev Translator := Expr → TranslationM (Option Term)
-
-namespace Translator
-
-private unsafe def getTranslatorsUnsafe : MetaM (List (Translator × Name)) := do
-  let env ← getEnv
-  let names := ((smtExt.getState env).findD ``Translator {}).toList
-  -- trace[smt.debug.attr] "Translators: {names}"
-  let mut translators := []
-  for name in names do
-    let fn ← IO.ofExcept <| Id.run <| ExceptT.run <|
-      env.evalConst Translator Options.empty name
-    translators := (fn, name) :: translators
-  return translators
-
-/-- Returns the list of translators maintained by `smtExt` in the current
-    Lean environment. -/
-@[implemented_by getTranslatorsUnsafe]
-opaque getTranslators : MetaM (List (Translator × Name))
-
-/-- Return a cached translation of `e` if found, otherwise run `k e` and cache the result. -/
-def withCache (k : Translator) (e : Expr) : TranslationM (Option Term) := do
-  match (← get).cache.find? e with
-  | some (some (tm, deps)) =>
-    modify fun st => { st with depConstants := st.depConstants.union deps }
-    return some tm
-  | some none =>
-    return none
-  | none =>
-    let depConstantsBefore := (← get).depConstants
-    modify fun st => { st with depConstants := .empty }
-    let ret? ← k e
-    modify fun st => { st with
-      depConstants := st.depConstants.union depConstantsBefore
-      cache := st.cache.insert e <| ret?.map ((·, st.depConstants))
-    }
-    return ret?
-
-mutual
-
-/-- Like `applyTranslators?` but must succeed. -/
-partial def applyTranslators! (e : Expr) : TranslationM Term := do
-  let some tm ← applyTranslators? e | throwError "no translator matched {e}"
-  return tm
-
-/-- Traverses `e` to compute its SMT-LIB translation. First all translators are tried on the whole
-expression and if one succeeds, its result is returned. Otherwise, `e` is split into subexpressions
-which are then recursively translated and put together into an SMT-LIB term. The traversal proceeds
-in a top-down, depth-first order. -/
-partial def applyTranslators? : Translator := withCache fun e => do
-  let ts ← getTranslators
-  go ts e
-  where
-    go (ts : List (Translator × Name)) : Translator := fun e => do
-      -- First try all translators on the whole expression
-      -- TODO: Use `DiscrTree` to index the translators instead of naively looping
-      for (t, nm) in ts do
-        if let some tm ← t e then
-          trace[smt.debug.translate.expr] "{e} =({nm})=> {tm}"
-          return tm
-
-      -- Then try splitting subexpressions
-      match e with
-      | fvar fv =>
-        let ld ← fv.getDecl
-        return symbolT ld.userName.toString
-      | const nm _ =>
-        modify fun st => { st with depConstants := st.depConstants.insert nm }
-        return symbolT nm.toString
-      | app f e => return appT (← applyTranslators! f) (← applyTranslators! e)
-      | lam .. => throwError "cannot translate {e}, SMT-LIB does not support lambdas"
-      | forallE n t b bi =>
-        let tmB ← Meta.withLocalDecl n bi t (fun x => applyTranslators! <| b.instantiate #[x])
-        if !b.hasLooseBVars /- not a dependent arrow -/ then
-          return arrowT (← applyTranslators! t) tmB
-        else
-          return forallT n.toString (← applyTranslators! t) tmB
-      | letE n t v b _ =>
-        let tmB ← Meta.withLetDecl n t v (fun x => applyTranslators! <| b.instantiate #[x])
-        return letT n.toString (← applyTranslators! v) tmB
-      | mdata _ e => go ts e
-      | e         => throwError "cannot translate {e}"
-
-end
-
-def traceTranslation (e : Expr) (e' : Except ε (Term × NameSet)) : TranslationM MessageData :=
-  return m!"{e} ↦ " ++ match e' with
-    | .ok (e', _) => m!"{e'}"
-    | .error _    => m!"{bombEmoji}"
-
-/-- Processes `e` by running it through all the registered `Translator`s.
-Returns the resulting SMT-LIB term and set of dependencies. -/
-def translateExpr (e : Expr) : TranslationM (Term × NameSet) :=
-  withTraceNode `smt.debug.translate (traceTranslation e ·) do
-    modify fun st => { st with depConstants := .empty }
-    trace[smt.debug.translate.expr] "before: {e}"
-    let tm ← applyTranslators! e
-    trace[smt.debug.translate.expr] "translated: {tm}"
-    return (tm, (← get).depConstants)
-
-def translateExpr' (e : Expr) : TranslationM Term :=
-  Prod.fst <$> translateExpr e
-
-end Smt.Translator
diff --git a/Smt/UF.lean b/Smt/UF.lean
new file mode 100644
index 00000000..36b19b17
--- /dev/null
+++ b/Smt/UF.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Reconstruct.UF