diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml
deleted file mode 100644
index b83b5acb..00000000
--- a/src/backend/Backend_intf.ml
+++ /dev/null
@@ -1,29 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** Backend interface
-
-    This modules defines the interface of the modules providing
-    export of proofs.
-*)
-
-module type S = sig
-  (** Proof exporting
-
-      Currently, exporting a proof means printing it into a file
-      according to the conventions of a given format.
-  *)
-
-  type store
-
-  type t
-  (** The type of proofs. *)
-
-  val pp : store -> Format.formatter -> t -> unit
-  (** A function for printing proofs in the desired format. *)
-
-end
-
diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml
deleted file mode 100644
index e8f2f8e1..00000000
--- a/src/backend/Dot.ml
+++ /dev/null
@@ -1,156 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** Output interface for the backend *)
-module type S = Backend_intf.S
-
-(** Input module for the backend *)
-module type Arg = sig
-
-  type atom
-  (* Type of atoms *)
-
-  type store
-  type hyp
-  type lemma
-  type assumption
-  (** Types for hypotheses, lemmas, and assumptions. *)
-
-  val print_atom : store -> Format.formatter -> atom -> unit
-  (** Printing function for atoms *)
-
-  val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list
-  val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list
-  val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list
-  (** Functions to return information about hypotheses and lemmas *)
-
-end
-
-module Default(S : Sidekick_sat.S) = struct
-  module Atom = S.Atom
-  module Clause = S.Clause
-
-  type store = S.solver
-  let print_atom = S.Atom.pp
-
-  let hyp_info store c =
-    "hypothesis", Some "LIGHTBLUE",
-    [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
-
-  let lemma_info store c =
-    "lemma", Some "BLUE",
-    [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
-
-  let assumption_info store c =
-    "assumption", Some "PURPLE",
-    [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
-
-end
-
-(** Functor to provide dot printing *)
-module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
-                                and type hyp := S.clause
-                                and type lemma := S.clause
-                                and type store := S.store
-                                and type assumption := S.clause) = struct
-  module Atom = S.Atom
-  module Clause = S.Clause
-  module P = S.Proof
-
-  let node_id store n = S.Clause.short_name store n.P.conclusion
-  let proof_id store p = node_id store (P.expand store p)
-  let res_nn_id store n1 n2 = node_id store n1 ^ "_" ^ node_id store n2 ^ "_res"
-  let res_np_id store n1 n2 = node_id store n1 ^ "_" ^ proof_id store n2 ^ "_res"
-
-  let print_clause store fmt c =
-    let v = S.Clause.atoms_a store c in
-    if Array.length v = 0 then
-      Format.fprintf fmt "⊥"
-    else
-      let n = Array.length v in
-      for i = 0 to n - 1 do
-        Format.fprintf fmt "%a" (A.print_atom store) v.(i);
-        if i < n - 1 then
-          Format.fprintf fmt ", "
-      done
-
-  let print_edge fmt i j =
-    Format.fprintf fmt "%s -> %s;@\n" j i
-
-  let print_edges store fmt n =
-    match P.(n.step) with
-    | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *)
-    | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
-      print_edge fmt (res_np_id store n p0) (proof_id store hr_init);
-      List.iter
-        (fun (_,p2) -> print_edge fmt (res_np_id store n p2) (proof_id store p2))
-        l;
-    | _ -> ()
-
-  let table_options fmt color =
-    Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
-
-  let table store fmt (c, rule, color, l) =
-    Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" (print_clause store) c;
-    match l with
-    | [] ->
-      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
-    | f :: r ->
-      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
-        color (List.length l) rule f ();
-      List.iter (fun f -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" f ()) r
-
-  let print_dot_node store fmt id color c rule rule_color l =
-    Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\n"
-      id table_options color (table store) (c, rule, rule_color, l)
-
-  let print_dot_res_node store fmt id a =
-    Format.fprintf fmt "%s [label=<%a>];@\n" id (A.print_atom store) a
-
-  let ttify f c = fun fmt () -> f fmt c
-
-  let print_contents store fmt n =
-    match P.(n.step) with
-    (* Leafs of the proof tree *)
-    | P.Hypothesis _ ->
-      let rule, color, l = A.hyp_info store P.(n.conclusion) in
-      let color = match color with None -> "LIGHTBLUE" | Some c -> c in
-      print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
-    | P.Assumption ->
-      let rule, color, l = A.assumption_info store P.(n.conclusion) in
-      let color = match color with None -> "LIGHTBLUE" | Some c -> c in
-      print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
-    | P.Lemma _ ->
-      let rule, color, l = A.lemma_info store P.(n.conclusion) in
-      let color = match color with None -> "YELLOW" | Some c -> c in
-      print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
-
-    (* Tree nodes *)
-    | P.Duplicate (p, l) ->
-      print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Duplicate" "GREY"
-        ((fun fmt () -> (Format.fprintf fmt "%s" (node_id store n))) ::
-         List.map (ttify @@ A.print_atom store) l);
-      print_edge fmt (node_id store n) (node_id store (P.expand store p))
-    | P.Hyper_res {P.hr_steps=l; _} ->
-      print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Resolution" "GREY"
-        [(fun fmt () -> (Format.fprintf fmt "%s" (node_id store n)))];
-      List.iter
-        (fun (a,p2) ->
-          print_dot_res_node store fmt (res_np_id store n p2) a;
-          print_edge fmt (node_id store n) (res_np_id store n p2))
-        l
-
-  let print_node store fmt n =
-    print_contents store fmt n;
-    print_edges store fmt n
-
-  let pp store fmt p =
-    Format.fprintf fmt "digraph proof {@\n";
-    P.fold store (fun () -> print_node store fmt) () p;
-    Format.fprintf fmt "}@."
-
-end
-
diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli
deleted file mode 100644
index 11bd9a7d..00000000
--- a/src/backend/Dot.mli
+++ /dev/null
@@ -1,67 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** Dot backend for proofs
-
-    This module provides functions to export proofs into the dot graph format.
-    Graphs in dot format can be used to generates images using the graphviz tool.
-*)
-
-module type S = Backend_intf.S
-(** Interface for exporting proofs. *)
-
-module type Arg = sig
-  (** Term printing for DOT
-
-      This module defines what functions are required in order to export
-      a proof to the DOT format.
-  *)
-
-  type atom
-  (** The type of atomic formuals *)
-
-  type hyp
-  type lemma
-  type assumption
-  (** The type of theory-specifi proofs (also called lemmas). *)
-
-  type store
-
-  val print_atom : store -> Format.formatter -> atom -> unit
-  (** Print the contents of the given atomic formulas.
-      WARNING: this function should take care to escape and/or not output special
-      reserved characters for the dot format (such as quotes and so on). *)
-
-  val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list
-  val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list
-  val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list
-  (** Generate some information about the leafs of the proof tree. Currently this backend
-      print each lemma/assumption/hypothesis as a single leaf of the proof tree.
-      These function should return a triplet [(rule, color, l)], such that:
-      - [rule] is a name for the proof (arbitrary, does not need to be unique, but
-        should rather be descriptive)
-      - [color] is a color name (optional) understood by DOT
-      - [l] is a list of printers that will be called to print some additional information
-  *)
-
-end
-
-module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
-                                 and type hyp := S.clause
-                                 and type lemma := S.clause
-                                 and type store := S.store
-                                 and type assumption := S.clause
-(** Provides a reasonnable default to instantiate the [Make] functor, assuming
-    the original printing functions are compatible with DOT html labels. *)
-
-module Make(S : Sidekick_sat.S)
-    (A : Arg with type atom := S.atom
-       and type hyp := S.clause
-       and type lemma := S.clause
-       and type store := S.store
-       and type assumption := S.clause)
-  : S with type t := S.Proof.t and type store := S.store
-(** Functor for making a module to export proofs to the DOT format. *)
diff --git a/src/backend/dune b/src/backend/dune
deleted file mode 100644
index 93b0e234..00000000
--- a/src/backend/dune
+++ /dev/null
@@ -1,7 +0,0 @@
-(library
-  (name sidekick_backend)
-  (public_name sidekick.backend)
-  (synopsis "Proof backends for sidekick")
-  (flags :standard -warn-error -a+8)
-  (libraries sidekick.sat))
-
diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 941d5507..de98a67f 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -15,18 +15,18 @@ module type S = Sidekick_core.CC_S
 module Make (A: CC_ARG)
   : S with module T = A.T
        and module Lit = A.Lit
-       and module P = A.P
+       and type lemma = A.lemma
        and module Actions = A.Actions
 = struct
   module T = A.T
-  module P = A.P
   module Lit = A.Lit
   module Actions = A.Actions
+  module P = Actions.P
   type term = T.Term.t
   type term_store = T.Term.store
   type lit = Lit.t
   type fun_ = T.Fun.t
-  type proof = P.t
+  type lemma = A.lemma
   type actions = Actions.t
 
   module Term = T.Term
@@ -95,7 +95,6 @@ module Make (A: CC_ARG)
     | E_congruence of node * node (* caused by normal congruence *)
     | E_and of explanation * explanation
     | E_theory of explanation
-    | E_proof of P.t
 
   type repr = node
 
@@ -169,7 +168,6 @@ module Make (A: CC_ARG)
       | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
       | E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
       | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
-      | E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" (P.pp_debug ~sharing:false) p
       | E_and (a,b) ->
         Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
 
@@ -179,7 +177,6 @@ module Make (A: CC_ARG)
     let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b)
     let[@inline] mk_lit l : t = E_lit l
     let mk_theory e = E_theory e
-    let mk_proof p = E_proof p
 
     let rec mk_list l =
       match l with
@@ -283,7 +280,7 @@ module Make (A: CC_ARG)
   and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
   and ev_on_new_term = t -> N.t -> term -> unit
   and ev_on_conflict = t -> th:bool -> lit list -> unit
-  and ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit
+  and ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit
   and ev_on_is_subterm = N.t -> term -> unit
 
   let[@inline] size_ (r:repr) = r.n_size
@@ -310,16 +307,8 @@ module Make (A: CC_ARG)
      Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *)
   let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
 
-  let ret_cc_lemma _what _lits p_lits =
-    let p = P.cc_lemma p_lits in
-    (* useful to debug bad lemmas
-    let n_pos = Iter.of_list p_lits |> Iter.filter P.lit_sign |> Iter.length in
-    if n_pos <> 1 then (
-      Log.debugf 0 (fun k->k"emit (n-pos=%d) :from %s@ %a@ :lits %a"
-                       n_pos what
-                       (P.pp_debug ~sharing:false) p Fmt.(Dump.list Lit.pp) lits);
-    );
-    *)
+  let ret_cc_lemma _what (_lits:lit list) (p_lits:lit Iter.t) =
+    let p = P.lemma_cc p_lits in
     p
 
   (* print full state *)
@@ -473,9 +462,6 @@ module Make (A: CC_ARG)
     | E_lit lit -> lit :: acc
     | E_theory e' ->
       th := true; explain_decompose_expl cc ~th acc e'
-    | E_proof _p ->
-      (* FIXME: need to also return pairs of [t, u, |-t=u] as part of explanation *)
-      assert false
     | E_merge (a,b) -> explain_equal cc ~th acc a b
     | E_merge_t (a,b) ->
       (* find nodes for [a] and [b] on the fly *)
@@ -676,14 +662,8 @@ module Make (A: CC_ARG)
         let lits = explain_equal cc ~th lits a ra in
         let lits = explain_equal cc ~th lits b rb in
         let proof =
-          let p_lits =
-            lits
-            |> List.rev_map (fun lit ->
-                let t, sign = Lit.signed_term lit in
-                P.lit_mk (not sign) t)
-          in
-          ret_cc_lemma "true-eq-false" lits p_lits
-        in
+          let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
+          ret_cc_lemma "true-eq-false" lits p_lits in
         raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof
       );
       (* We will merge [r_from] into [r_into].
@@ -801,10 +781,7 @@ module Make (A: CC_ARG)
                let lits = explain_equal cc ~th acc u1 t1 in
                let p_lits =
                  (* make a tautology, not a true guard *)
-                 let tauto = lit :: List.rev_map Lit.neg lits in
-                 tauto |> List.rev_map (fun lit ->
-                     let t, sign = Lit.signed_term lit in
-                     A.P.(lit_mk sign t))
+                 Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg)
                in
                let p = ret_cc_lemma "bool-parent" lits p_lits in
                lits, p
@@ -875,11 +852,7 @@ module Make (A: CC_ARG)
     let lits = explain_decompose_expl cc ~th [] expl in
     let lits = List.rev_map Lit.neg lits in
     let proof =
-      let p_lits =
-        lits |> List.rev_map (fun lit ->
-            let t, sign = Lit.signed_term lit in
-            P.lit_mk sign t)
-      in
+      let p_lits = Iter.of_list lits in
       ret_cc_lemma "from-expl" lits p_lits
     in
     raise_conflict_ cc ~th:!th acts lits proof
diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli
index 6201f09e..21566fc7 100644
--- a/src/cc/Sidekick_cc.mli
+++ b/src/cc/Sidekick_cc.mli
@@ -4,7 +4,7 @@ open Sidekick_core
 module type S = Sidekick_core.CC_S
 
 module Make (A: CC_ARG)
-  : S with module T = A.T 
+  : S with module T = A.T
        and module Lit = A.Lit
-       and module P = A.P
+       and type lemma = A.lemma
        and module Actions = A.Actions
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 84a58527..69fc3256 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -145,89 +145,37 @@ module type TERM = sig
   end
 end
 
-(** Proofs of unsatisfiability *)
+(** Proofs for the congruence closure *)
+module type CC_PROOF = sig
+  type lit
+  type lemma
+
+  val lemma_cc : lit Iter.t -> lemma
+end
+
+(* TODO: use same proofs as Sidekick_sat?
+
+   but give more precise type to [lemma]? *)
+(** Proofs of unsatisfiability.
+
+    We use DRUP(T)-style traces where we simply emit clauses as we go,
+    annotating enough for the checker to reconstruct them.
+    This allows for low overhead proof production. *)
 module type PROOF = sig
   type t
   (** The abstract representation of a proof. A proof always proves
       a clause to be {b valid} (true in every possible interpretation
       of the problem's assertions, and the theories) *)
 
-  type term
-  type ty
-
-  type hres_step
-  (** hyper-resolution steps: resolution, unit resolution;
-      bool paramodulation, unit bool paramodulation *)
-
-  val r : t -> pivot:term -> hres_step
-  (** Resolution step on given pivot term *)
-
-  val r1 : t -> hres_step
-  (** Unit resolution; pivot is obvious *)
-
-  val p : t -> lhs:term -> rhs:term -> hres_step
-  (** Paramodulation using proof whose conclusion has a literal [lhs=rhs] *)
-
-  val p1 : t -> hres_step
-  (** Unit paramodulation *)
+  type lemma
 
   type lit
-  (** Proof representation of literals *)
 
-  val pp_lit : lit Fmt.printer
-  val lit_a : term -> lit
-  val lit_na : term -> lit
-  val lit_mk : bool -> term -> lit
-  val lit_eq : term -> term -> lit
-  val lit_neq : term -> term -> lit
-  val lit_not : lit -> lit
-  val lit_sign : lit -> bool
+  include CC_PROOF
+    with type lemma := lemma
+     and type lit := lit
 
-  type composite_step
-
-  val stepc : name:string -> lit list -> t -> composite_step
-  val deft : term -> term -> composite_step (** define a (new) atomic term *)
-
-  val is_trivial_refl : t -> bool
-  (** is this a proof of [|- t=t]? This can be used to remove
-      some trivial steps that would build on the proof (e.g. rewriting
-      using [refl t] is useless). *)
-
-  val assertion : term -> t
-  val assertion_c : lit Iter.t -> t
-  val ref_by_name : string -> t (* named clause, see {!defc} *)
-  val assertion_c_l : lit list -> t
-  val drup_res : lit list -> t (* assert clause and let DRUP take care of it *)
-  val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *)
-  val hres_l : t -> hres_step list -> t (* hyper-res *)
-  val res : pivot:term -> t -> t -> t (* resolution with pivot *)
-  val res1 : t -> t -> t (* unit resolution *)
-  val refl : term -> t (* proof of [| t=t] *)
-  val true_is_true : t (* proof of [|- true] *)
-  val true_neq_false : t (* proof of [|- not (true=false)] *)
-  val nn : t -> t (* negation normalization *)
-  val cc_lemma : lit list -> t (* equality tautology, unsigned *)
-  val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *)
-  val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *)
-  val composite_iter : ?assms:(string * lit) list -> composite_step Iter.t -> t
-  val composite_l : ?assms:(string * lit) list -> composite_step list -> t
-  val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
-  val sorry_c : lit Iter.t -> t
-  [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
-
-  val sorry_c_l : lit list -> t
-
-  val default : t [@@alert cstor "do not use default constructor"]
-
-  val pp_debug : sharing:bool -> t Fmt.printer
-  (** Pretty print a proof.
-      @param sharing if true, try to compact the proof by introducing
-      definitions for common terms, clauses, and steps as needed. Safe to ignore. *)
-
-  module Quip : sig
-    val output : out_channel -> t -> unit
-    (** Printer in Quip format (experimental) *)
-  end
+  val enabled : t -> bool
 end
 
 (** Literals
@@ -274,20 +222,21 @@ module type CC_ACTIONS = sig
   module T : TERM
   module Lit : LIT with module T = T
 
-  module P : PROOF with type term = T.Term.t
+  type lemma
+  module P : CC_PROOF with type lit = Lit.t and type lemma = lemma
 
   type t
   (** An action handle. It is used by the congruence closure
       to perform the actions below. How it performs the actions
       is not specified and is solver-specific. *)
 
-  val raise_conflict : t -> Lit.t list -> P.t -> 'a
+  val raise_conflict : t -> Lit.t list -> lemma -> 'a
   (** [raise_conflict acts c pr] declares that [c] is a tautology of
       the theory of congruence. This does not return (it should raise an
       exception).
       @param pr the proof of [c] being a tautology *)
 
-  val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * P.t) -> unit
+  val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * lemma) -> unit
   (** [propagate acts lit ~reason pr] declares that [reason() => lit]
       is a tautology.
 
@@ -301,15 +250,19 @@ end
 (** Arguments to a congruence closure's implementation *)
 module type CC_ARG = sig
   module T : TERM
-  module P : PROOF with type term = T.Term.t
   module Lit : LIT with module T = T
-  module Actions : CC_ACTIONS with module T=T and module P = P and module Lit = Lit
+  type lemma
+  module P : CC_PROOF with type lit = Lit.t and type lemma = lemma
+  module Actions : CC_ACTIONS
+    with module T=T
+     and module Lit = Lit
+     and type lemma = lemma
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
   (** View the term through the lens of the congruence closure *)
 end
 
-(** Main congruence closure.
+(** Main congruence closure signature.
 
     The congruence closure handles the theory QF_UF (uninterpreted
     function symbols).
@@ -329,14 +282,17 @@ module type CC_S = sig
   (** first, some aliases. *)
 
   module T : TERM
-  module P : PROOF with type term = T.Term.t
   module Lit : LIT with module T = T
-  module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P
+  type lemma
+  module P : CC_PROOF with type lit = Lit.t and type lemma = lemma
+  module Actions : CC_ACTIONS
+    with module T = T
+    and module Lit = Lit
+    and type lemma = lemma
   type term_store = T.Term.store
   type term = T.Term.t
   type fun_ = T.Fun.t
   type lit = Lit.t
-  type proof = P.t
   type actions = Actions.t
 
   type t
@@ -421,7 +377,6 @@ module type CC_S = sig
     val mk_merge_t : term -> term -> t
     val mk_lit : lit -> t
     val mk_list : t list -> t
-    val mk_proof : P.t -> t
     val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *)
   end
 
@@ -474,7 +429,7 @@ module type CC_S = sig
       participating in the conflict are purely syntactic theories
       like injectivity of constructors. *)
 
-  type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit
+  type ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit
   (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
       is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
 
@@ -620,12 +575,22 @@ end
     new lemmas, propagate literals, access the congruence closure, etc. *)
 module type SOLVER_INTERNAL = sig
   module T : TERM
-  module P : PROOF with type term = T.Term.t
 
   type ty = T.Ty.t
   type term = T.Term.t
   type term_store = T.Term.store
   type ty_store = T.Ty.store
+
+  (** {3 Literals}
+
+      A literal is a (preprocessed) term along with its sign.
+      It is directly manipulated by the SAT solver.
+  *)
+  module Lit : LIT with module T = T
+
+  (** {3 Proofs} *)
+  type lemma
+  module P : PROOF with type lit = Lit.t and type lemma = lemma
   type proof = P.t
 
   (** {3 Main type for a solver} *)
@@ -641,13 +606,6 @@ module type SOLVER_INTERNAL = sig
   type actions
   (** Handle that the theories can use to perform actions. *)
 
-  (** {3 Literals}
-
-      A literal is a (preprocessed) term along with its sign.
-      It is directly manipulated by the SAT solver.
-  *)
-  module Lit : LIT with module T = T
-
   type lit = Lit.t
 
   (** {3 Proof helpers} *)
@@ -662,8 +620,10 @@ module type SOLVER_INTERNAL = sig
   (** Congruence closure instance *)
   module CC : CC_S
     with module T = T
-     and module P = P
      and module Lit = Lit
+     and type lemma = lemma
+     and type P.lemma = lemma
+     and type P.lit = lit
      and type Actions.t = actions
 
   val cc : t -> CC.t
@@ -872,15 +832,16 @@ end
     Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *)
 module type SOLVER = sig
   module T : TERM
-  module P : PROOF with type term = T.Term.t
-
   module Lit : LIT with module T = T
+  type lemma
+  module P : PROOF with type lit = Lit.t and type lemma = lemma
 
   module Solver_internal
     : SOLVER_INTERNAL
       with module T = T
-       and module P = P
        and module Lit = Lit
+       and type lemma = lemma
+       and module P = P
   (** Internal solver, available to theories.  *)
 
   type t
diff --git a/src/msat-solver/dune b/src/msat-solver/dune
index 78d55808..8e6100cd 100644
--- a/src/msat-solver/dune
+++ b/src/msat-solver/dune
@@ -2,5 +2,5 @@
  (name Sidekick_msat_solver)
  (public_name sidekick.msat-solver)
  (libraries containers iter sidekick.core sidekick.util
-            sidekick.cc sidekick.sat sidekick.backend)
+            sidekick.cc sidekick.sat)
  (flags :standard -open Sidekick_util))
diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index 089e88ea..0c119711 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -34,10 +34,12 @@ end
 module Make(Plugin : PLUGIN)
 = struct
   module Formula = Plugin.Formula
+  module Proof = Plugin.Proof
 
   type formula = Formula.t
   type theory = Plugin.t
-  type lemma = Plugin.proof
+  type lemma = Plugin.lemma
+  type proof = Plugin.proof
 
   (* ### types ### *)
 
@@ -511,279 +513,6 @@ module Make(Plugin : PLUGIN)
   module Var = Store.Var
   module Clause = Store.Clause
 
-  (* TODO: mostly, move into a functor outside that works on integers *)
-  module Proof =  struct
-    exception Resolution_error of string
-
-    type atom = Atom.t
-    type clause = Clause.t
-    type formula = Formula.t
-    type lemma = Plugin.proof
-    type nonrec store = store
-
-    let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg
-
-    let[@inline] clear_var_of_ store (a:atom) = Store.clear_var store (Atom.var a)
-
-    (* Compute resolution of 2 clauses.
-       returns [pivots, resulting_atoms] *)
-    let resolve store (c1:clause) (c2:clause) : atom list * atom list =
-      (* invariants: only atoms in [c2] are marked, and the pivot is
-         cleared when traversing [c1] *)
-      Clause.iter store c2 ~f:(Atom.mark store);
-      let pivots = ref [] in
-      let l =
-        Clause.fold store [] c1
-          ~f:(fun l a ->
-             if Atom.marked store a then l
-             else if Atom.marked store (Atom.neg a) then (
-               pivots := (Atom.abs a) :: !pivots;
-               clear_var_of_ store a;
-               l
-             ) else a::l)
-      in
-      let l =
-        Clause.fold store l c2
-          ~f:(fun l a -> if Atom.marked store a then a::l else l)
-      in
-      Clause.iter store c2 ~f:(clear_var_of_ store);
-      !pivots, l
-
-    (* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *)
-    let find_dups (store:store) (c:clause) : atom list * atom list =
-      let res =
-        Clause.fold store ([], []) c
-          ~f:(fun (dups,l) a ->
-             if Atom.marked store a then (
-               a::dups, l
-             ) else (
-               Atom.mark store a;
-               dups, a::l
-             ))
-      in
-      Clause.iter store c ~f:(clear_var_of_ store);
-      res
-
-    (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *)
-    let same_lits store (c1:atom Iter.t) (c2:atom Iter.t): bool =
-      let subset a b =
-        Iter.iter (Atom.mark store) b;
-        let res = Iter.for_all (Atom.marked store) a in
-        Iter.iter (clear_var_of_ store) b;
-        res
-      in
-      subset c1 c2 && subset c2 c1
-
-    let prove (store:store) conclusion =
-      match Clause.premise store conclusion with
-      | History [] -> assert false
-      | Empty_premise -> raise Solver_intf.No_proof
-      | _ -> conclusion
-
-    let rec set_atom_proof store a =
-      let aux acc b =
-        if Atom.equal (Atom.neg a) b then acc
-        else set_atom_proof store b :: acc
-      in
-      assert (Var.level store (Atom.var a) >= 0);
-      match Var.reason store (Atom.var a) with
-      | Some (Bcp c | Bcp_lazy (lazy c)) ->
-        Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])"
-                         (Atom.debug store) a (Clause.debug store) c);
-        if Clause.n_atoms store c = 1 then (
-          Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])"
-                           (Atom.debug store) a);
-          c
-        ) else (
-          assert (Atom.is_false store a);
-          let r = History (c :: (Clause.fold store [] c ~f:aux)) in
-          let c' = Clause.make_l store ~removable:false [Atom.neg a] r in
-          Var.set_reason store (Atom.var a) (Some (Bcp c'));
-          Log.debugf 5
-            (fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])"
-                (Atom.debug store) a (Clause.debug store) c');
-          c'
-        )
-      | _ ->
-        error_res_f "cannot prove atom %a" (Atom.debug store) a
-
-    let prove_unsat store conflict =
-      if Clause.n_atoms store conflict = 0 then (
-        conflict
-      ) else (
-        Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" (Clause.debug store) conflict);
-        let l = Clause.fold store [] conflict
-            ~f:(fun acc a -> set_atom_proof store a :: acc) in
-        let res = Clause.make_l store ~removable:false [] (History (conflict :: l)) in
-        Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" (Clause.debug store) res);
-        res
-      )
-
-    let prove_atom self a =
-      if Atom.is_true self a &&
-         Var.level self (Atom.var a) = 0 then
-        Some (set_atom_proof self a)
-      else
-        None
-
-    type t = clause
-    and proof_node = {
-      conclusion : clause;
-      step : step;
-    }
-    and step =
-      | Hypothesis of lemma
-      | Assumption
-      | Lemma of lemma
-      | Duplicate of t * atom list
-      | Hyper_res of hyper_res_step
-
-    and hyper_res_step = {
-      hr_init: t;
-      hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
-    }
-
-    let[@inline] conclusion (p:t) : clause = p
-
-    (* find pivots for resolving [l] with [init], and also return
-       the atoms of the conclusion *)
-    let find_pivots store (init:clause) (l:clause list) : _ * (atom * t) list =
-      Log.debugf 15
-        (fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])"
-            (Clause.debug store) init (Format.pp_print_list (Clause.debug store)) l);
-      Clause.iter store init ~f:(Atom.mark store);
-      let steps =
-        List.map
-          (fun c ->
-             let pivot =
-               match
-                 Clause.atoms_iter store c
-                 |> Iter.filter (fun a -> Atom.marked store (Atom.neg a))
-                 |> Iter.to_list
-               with
-                 | [a] -> a
-                 | [] ->
-                   error_res_f "(@[proof.expand.pivot_missing@ %a@])" (Clause.debug store) c
-                 | pivots ->
-                   error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])"
-                     (Clause.debug store) c (Atom.debug_l store) pivots
-             in
-             Clause.iter store c ~f:(Atom.mark store); (* add atoms to result *)
-             clear_var_of_ store pivot;
-             Atom.abs pivot, c)
-          l
-      in
-      (* cleanup *)
-      let res = ref [] in
-      let cleanup_a_ a =
-        if Atom.marked store a then (
-          res := a :: !res;
-          clear_var_of_ store a
-        )
-      in
-      Clause.iter store init ~f:cleanup_a_;
-      List.iter (fun c -> Clause.iter store c ~f:cleanup_a_) l;
-      !res, steps
-
-    let expand store conclusion =
-      Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" (Clause.debug store) conclusion);
-      match Clause.premise store conclusion with
-      | Lemma l ->
-        { conclusion; step = Lemma l; }
-      | Local ->
-        { conclusion; step = Assumption; }
-      | Hyp l ->
-        { conclusion; step = Hypothesis l; }
-      | History [] ->
-        error_res_f "@[empty history for clause@ %a@]" (Clause.debug store) conclusion
-      | History [c] ->
-        let duplicates, res = find_dups store c in
-        assert (same_lits store (Iter.of_list res) (Clause.atoms_iter store conclusion));
-        { conclusion; step = Duplicate (c, duplicates) }
-      | History (c :: r) ->
-        let res, steps = find_pivots store c r in
-        assert (same_lits store (Iter.of_list res) (Clause.atoms_iter store conclusion));
-        { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps};  }
-      | Empty_premise -> raise Solver_intf.No_proof
-
-    let rec res_of_hyper_res store (hr: hyper_res_step) : _ * _ * atom =
-      let {hr_init=c1; hr_steps=l} = hr in
-      match l with
-      | [] -> assert false
-      | [a, c2] -> c1, c2, a (* done *)
-      | (a,c2) :: steps' ->
-        (* resolve [c1] with [c2], then resolve that against [steps] *)
-        let pivots, l = resolve store c1 c2 in
-        assert (match pivots with [a'] -> Atom.equal a a' | _ -> false);
-        let c_1_2 = Clause.make_l store ~removable:true l (History [c1; c2]) in
-        res_of_hyper_res store {hr_init=c_1_2; hr_steps=steps'}
-
-    (* Proof nodes manipulation *)
-    let is_leaf = function
-      | Hypothesis _
-      | Assumption
-      | Lemma _ -> true
-      | Duplicate _
-      | Hyper_res _ -> false
-
-    let parents = function
-      | Hypothesis _
-      | Assumption
-      | Lemma _ -> []
-      | Duplicate (p, _) -> [p]
-      | Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps
-
-    let expl = function
-      | Hypothesis _ -> "hypothesis"
-      | Assumption -> "assumption"
-      | Lemma _ -> "lemma"
-      | Duplicate _ -> "duplicate"
-      | Hyper_res _ -> "hyper-resolution"
-
-    module Tbl = Clause.Tbl
-
-    type task =
-      | Enter of t
-      | Leaving of t
-
-    let spop s = try Some (Stack.pop s) with Stack.Empty -> None
-
-    let rec fold_aux self s h f acc =
-      match spop s with
-      | None -> acc
-      | Some (Leaving c) ->
-        Tbl.add h c true;
-        fold_aux self s h f (f acc (expand self c))
-      | Some (Enter c) ->
-        if not (Tbl.mem h c) then begin
-          Stack.push (Leaving c) s;
-          let node = expand self c in
-          begin match node.step with
-            | Duplicate (p1, _) ->
-              Stack.push (Enter p1) s
-            | Hyper_res {hr_init=p1; hr_steps=l} ->
-              List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l;
-              Stack.push (Enter p1) s;
-            | Hypothesis _ | Assumption | Lemma _ -> ()
-          end
-        end;
-        fold_aux self s h f acc
-
-    let fold self f acc p =
-      let h = Tbl.create 42 in
-      let s = Stack.create () in
-      Stack.push (Enter p) s;
-      fold_aux self s h f acc
-
-    let check_empty_conclusion store (p:t) =
-      if Clause.n_atoms store p > 0 then (
-        error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]"
-          (Clause.debug store) p;
-      )
-
-    let check self (p:t) = fold self (fun () _ -> ()) () p
-  end
-
   module H = (Heap.Make [@specialise]) (struct
     type store = Store.t
     type t = var
@@ -1775,7 +1504,8 @@ module Make(Plugin : PLUGIN)
 
   let[@inline] current_slice st : _ Solver_intf.acts =
     let module M = struct
-      type nonrec proof = lemma
+      type nonrec proof = proof
+      type nonrec lemma = lemma
       type nonrec formula = formula
       let iter_assumptions=acts_iter st ~full:false st.th_head
       let eval_lit= acts_eval_lit st
@@ -1790,7 +1520,8 @@ module Make(Plugin : PLUGIN)
   (* full slice, for [if_sat] final check *)
   let[@inline] full_slice st : _ Solver_intf.acts =
     let module M = struct
-      type nonrec proof = lemma
+      type nonrec proof = proof
+      type nonrec lemma = lemma
       type nonrec formula = formula
       let iter_assumptions=acts_iter st ~full:true st.th_head
       let eval_lit= acts_eval_lit st
diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli
index c6b8e28d..1af4efd8 100644
--- a/src/sat/Solver.mli
+++ b/src/sat/Solver.mli
@@ -4,10 +4,12 @@ module type S = Solver_intf.S
 
 module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
   : S with module Formula = Th.Formula
-       and type lemma = Th.proof
+       and type lemma = Th.lemma
+       and type proof = Th.proof
        and type theory = unit
 
 module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
   : S with module Formula = Th.Formula
-       and type lemma = Th.proof
+       and type lemma = Th.lemma
+       and type proof = Th.proof
        and type theory = Th.t
diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml
index 4622fc7c..cccd5f90 100644
--- a/src/sat/Solver_intf.ml
+++ b/src/sat/Solver_intf.ml
@@ -64,8 +64,8 @@ type negated =
     See {!val:Expr_intf.S.norm} for more details. *)
 
 (** The type of reasons for propagations of a formula [f]. *)
-type ('formula, 'proof) reason =
-  | Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
+type ('formula, 'lemma) reason =
+  | Consequence of (unit -> 'formula list * 'lemma) [@@unboxed]
   (** [Consequence (l, p)] means that the formulas in [l] imply the propagated
       formula [f]. The proof should be a proof of the clause "[l] implies [f]".
 
@@ -90,7 +90,7 @@ type lbool = L_true | L_false | L_undefined
 
 module type ACTS = sig
   type formula
-  type proof
+  type lemma
 
   val iter_assumptions: (formula -> unit) -> unit
   (** Traverse the new assumptions on the boolean trail. *)
@@ -102,19 +102,19 @@ module type ACTS = sig
   (** Map the given formula to a literal, which will be decided by the
       SAT solver. *)
 
-  val add_clause: ?keep:bool -> formula list -> proof -> unit
+  val add_clause: ?keep:bool -> formula list -> lemma -> unit
   (** Add a clause to the solver.
       @param keep if true, the clause will be kept by the solver.
         Otherwise the solver is allowed to GC the clause and propose this
         partial model again.
   *)
 
-  val raise_conflict: formula list -> proof -> 'b
+  val raise_conflict: formula list -> lemma -> 'b
   (** Raise a conflict, yielding control back to the solver.
       The list of atoms must be a valid theory lemma that is false in the
       current trail. *)
 
-  val propagate: formula -> (formula, proof) reason -> unit
+  val propagate: formula -> (formula, lemma) reason -> unit
   (** Propagate a formula, i.e. the theory can evaluate the formula to be true
       (see the definition of {!type:eval_res} *)
 
@@ -124,10 +124,9 @@ module type ACTS = sig
       Useful for theory combination. This will be undone on backtracking. *)
 end
 
-(* TODO: find a way to use atoms instead of formulas here *)
-type ('formula, 'proof) acts =
+type ('formula, 'lemma) acts =
   (module ACTS with type formula = 'formula
-                and type proof = 'proof)
+                and type lemma = 'lemma)
 (** The type for a slice of assertions to assume/propagate in the theory. *)
 
 exception No_proof
@@ -158,6 +157,45 @@ module type FORMULA = sig
       but one returns [Negated] and the other [Same_sign]. *)
 end
 
+(** Signature for proof emission, using DRUP.
+
+    We do not store the resolution steps, just the stream of clauses deduced.
+    See {!Sidekick_drup} for checking these proofs. *)
+module type PROOF = sig
+  type t
+  (** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
+
+  type atom
+  (** A boolean atom for the proof trace *)
+
+  type lemma
+  (** A theory lemma *)
+
+  module Atom : sig
+    type t = atom
+    val sign : t -> bool
+    val var_int : t -> int
+    val make : sign:bool -> int -> t
+    val pp : t Fmt.printer
+  end
+
+  val enabled : t -> bool
+  (** Do we emit proofs at all? *)
+
+  val emit_input_clause : t -> atom Iter.t -> unit
+  (** Emit an input clause. *)
+
+  val emit_lemma : t -> atom Iter.t -> lemma -> unit
+  (** Emit a theory lemma *)
+
+  val emit_redundant_clause : t -> atom Iter.t -> unit
+  (** Emit a clause deduced by the SAT solver, redundant wrt axioms.
+      The clause must be RUP wrt previous clauses. *)
+
+  val del_clause : t -> atom Iter.t -> unit
+  (** Forget a clause. Only useful for performance considerations. *)
+end
+
 (** Signature for theories to be given to the CDCL(T) solver *)
 module type PLUGIN_CDCL_T = sig
   type t
@@ -166,6 +204,14 @@ module type PLUGIN_CDCL_T = sig
   module Formula : FORMULA
 
   type proof
+  (** Proof storage/recording *)
+
+  type lemma
+  (* Theory lemmas *)
+
+  module Proof : PROOF
+    with type t = proof
+     and type lemma = lemma
 
   val push_level : t -> unit
   (** Create a new backtrack level *)
@@ -173,12 +219,12 @@ module type PLUGIN_CDCL_T = sig
   val pop_levels : t -> int -> unit
   (** Pop [n] levels of the theory *)
 
-  val partial_check : t -> (Formula.t, proof) acts -> unit
+  val partial_check : t -> (Formula.t, lemma) acts -> unit
   (** Assume the formulas in the slice, possibly using the [slice]
       to push new formulas to be propagated or to raising a conflict or to add
       new lemmas. *)
 
-  val final_check : t -> (Formula.t, proof) acts -> unit
+  val final_check : t -> (Formula.t, lemma) acts -> unit
   (** Called at the end of the search in case a model has been found.
       If no new clause is pushed, then proof search ends and "sat" is returned;
       if lemmas are added, search is resumed;
@@ -189,111 +235,12 @@ end
 module type PLUGIN_SAT = sig
   module Formula : FORMULA
 
+  type lemma = unit
   type proof
-end
 
-module type PROOF = sig
-  (** Signature for a module handling proof by resolution from sat solving traces *)
-
-  (** {3 Type declarations} *)
-
-  exception Resolution_error of string
-  (** Raised when resolution failed. *)
-
-  type formula
-  type atom
-  type lemma
-  type clause
-  (** Abstract types for atoms, clauses and theory-specific lemmas *)
-
-  type store
-
-  type t
-  (** Lazy type for proof trees. Proofs are persistent objects, and can be
-      extended to proof nodes using functions defined later. *)
-
-  and proof_node = {
-    conclusion : clause;  (** The conclusion of the proof *)
-    step : step;          (** The reasoning step used to prove the conclusion *)
-  }
-  (** A proof can be expanded into a proof node, which show the first step of the proof. *)
-
-  (** The type of reasoning steps allowed in a proof. *)
-  and step =
-    | Hypothesis of lemma
-    (** The conclusion is a user-provided hypothesis *)
-    | Assumption
-    (** The conclusion has been locally assumed by the user *)
-    | Lemma of lemma
-    (** The conclusion is a tautology provided by the theory, with associated proof *)
-    | Duplicate of t * atom list
-    (** The conclusion is obtained by eliminating multiple occurences of the atom in
-        the conclusion of the provided proof. *)
-    | Hyper_res of hyper_res_step
-
-  and hyper_res_step = {
-    hr_init: t;
-    hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
-  }
-
-  (** {3 Proof building functions} *)
-
-  val prove : store -> clause -> t
-  (** Given a clause, return a proof of that clause.
-      @raise Resolution_error if it does not succeed. *)
-
-  val prove_unsat : store -> clause -> t
-  (** Given a conflict clause [c], returns a proof of the empty clause.
-      @raise Resolution_error if it does not succeed. *)
-
-  val prove_atom : store -> atom -> t option
-  (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
-
-  val res_of_hyper_res : store -> hyper_res_step -> t * t * atom
-  (** Turn an hyper resolution step into a resolution step.
-      The conclusion can be deduced by performing a resolution between the conclusions
-      of the two given proofs.
-      The atom on which to perform the resolution is also given. *)
-
-  (** {3 Proof Nodes} *)
-
-  val parents : step -> t list
-  (** Returns the parents of a proof node. *)
-
-  val is_leaf : step -> bool
-  (** Returns wether the the proof node is a leaf, i.e. an hypothesis,
-      an assumption, or a lemma.
-      [true] if and only if {!parents} returns the empty list. *)
-
-  val expl : step -> string
-  (** Returns a short string description for the proof step; for instance
-      ["hypothesis"] for a [Hypothesis]
-      (it currently returns the variant name in lowercase). *)
-
-
-  (** {3 Proof Manipulation} *)
-
-  val expand : store -> t -> proof_node
-  (** Return the proof step at the root of a given proof. *)
-
-  val conclusion : t -> clause
-  (** What is proved at the root of the clause *)
-
-  val fold : store -> ('a -> proof_node -> 'a) -> 'a -> t -> 'a
-  (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
-      [f] is executed exactly once on each proof node in the tree, and that the execution of
-      [f] on a proof node happens after the execution on the parents of the nodes. *)
-
-  (** {3 Misc} *)
-
-  val check_empty_conclusion : store -> t -> unit
-  (** Check that the proof's conclusion is the empty clause,
-      @raise Resolution_error otherwise *)
-
-  val check : store -> t -> unit
-  (** Check the contents of a proof. Mainly for internal use. *)
-
-  module Tbl : Hashtbl.S with type key = t
+  module Proof : PROOF
+    with type t = proof
+     and type lemma = lemma
 end
 
 (** The external interface implemented by safe solvers, such as the one
@@ -317,11 +264,16 @@ module type S = sig
   type theory
 
   type lemma
-  (** A theory lemma or an input axiom *)
+  (** A theory lemma or an input axiom. *)
+
+  type proof
+  (** A representation of a full proof *)
 
   type solver
+  (** The main solver type. *)
 
   type store
+  (** Stores atoms, clauses, etc. *)
 
   (* TODO: keep this internal *)
   module Atom : sig
@@ -365,11 +317,9 @@ module type S = sig
   end
 
   module Proof : PROOF
-    with type clause = clause
-     and type atom = atom
-     and type formula = formula
+    with type atom = atom
      and type lemma = lemma
-     and type store = store
+     and type t = proof
   (** A module to manipulate proofs. *)
 
   type t = solver
diff --git a/src/smtlib/dune b/src/smtlib/dune
index 4476ec7a..e2b27b65 100644
--- a/src/smtlib/dune
+++ b/src/smtlib/dune
@@ -3,6 +3,5 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith sidekick.core sidekick.util
             sidekick-base sidekick-base.solver
-            sidekick.backend smtlib-utils
-            sidekick.tef)
+            smtlib-utils sidekick.tef)
  (flags :standard -warn-error -a+8 -open Sidekick_util))
diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml
index d568adfa..9bfb0fec 100644
--- a/src/th-cstor/Sidekick_th_cstor.ml
+++ b/src/th-cstor/Sidekick_th_cstor.ml
@@ -9,6 +9,7 @@ let name = "th-cstor"
 module type ARG = sig
   module S : Sidekick_core.SOLVER
   val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view
+  val lemma_cstor : S.Lit.t Iter.t -> S.lemma
 end
 
 module type S = sig