diff --git a/src/cc/CC.ml b/src/cc/CC.ml
index c8722d3f..004dec85 100644
--- a/src/cc/CC.ml
+++ b/src/cc/CC.ml
@@ -1,6 +1,6 @@
 open Types_
 
-type view_as_cc = Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
+type view_as_cc = Term.t -> (Const.t, Term.t, Term.t list) CC_view.t
 
 type e_node = E_node.t
 (** A node of the congruence closure *)
@@ -165,7 +165,7 @@ end
 
 (* compute up-to-date signature *)
 let update_sig (s : signature) : Signature.t =
-  View.map_view s ~f_f:(fun x -> x) ~f_t:find_ ~f_ts:(List.map find_)
+  CC_view.map_view s ~f_f:(fun x -> x) ~f_t:find_ ~f_ts:(List.map find_)
 
 (* find whether the given (parent) term corresponds to some signature
    in [signatures_] *)
@@ -466,19 +466,19 @@ and compute_sig0 (self : t) (n : e_node) : Signature.t option =
   | Eq (a, b) ->
     let a = deref_sub a in
     let b = deref_sub b in
-    return @@ View.Eq (a, b)
-  | Not u -> return @@ View.Not (deref_sub u)
+    return @@ CC_view.Eq (a, b)
+  | Not u -> return @@ CC_view.Not (deref_sub u)
   | App_fun (f, args) ->
-    let args = args |> Iter.map deref_sub |> Iter.to_list in
+    let args = List.map deref_sub args in
     if args <> [] then
-      return @@ View.App_fun (f, args)
+      return @@ CC_view.App_fun (f, args)
     else
       None
   | App_ho (f, a) ->
     let f = deref_sub f in
     let a = deref_sub a in
-    return @@ View.App_ho (f, a)
-  | If (a, b, c) -> return @@ View.If (deref_sub a, deref_sub b, deref_sub c)
+    return @@ CC_view.App_ho (f, a)
+  | If (a, b, c) -> return @@ CC_view.If (deref_sub a, deref_sub b, deref_sub c)
 
 let[@inline] add_term self t : e_node = add_term_rec_ self t
 let mem_term = mem
@@ -950,19 +950,9 @@ module Make (A : ARG) : BUILD = struct
     create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc
 end
 
-module Default = struct
-  include Make (struct
-    let view_as_cc (t : Term.t) : _ View.t =
-      let f, args = Term.unfold_app t in
-      match Term.view f, args with
-      | _, [ _; t; u ] when Term.is_eq f -> View.Eq (t, u)
-      | _ ->
-        (match Term.view t with
-        | Term.E_app (f, a) -> View.App_ho (f, a)
-        | Term.E_const c -> View.App_fun (c, Iter.empty)
-        | _ -> View.Opaque t)
-  end)
-end
+module Default = Make (Sidekick_core.Default_cc_view)
 
 let create (module A : ARG) ?stat ?size tst proof : t =
   create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc
+
+let create_default = Default.create
diff --git a/src/cc/CC.mli b/src/cc/CC.mli
index 9107db9e..4041f697 100644
--- a/src/cc/CC.mli
+++ b/src/cc/CC.mli
@@ -255,7 +255,7 @@ val pop_levels : t -> int -> unit
 val get_model : t -> E_node.t Iter.t Iter.t
 (** get all the equivalence classes so they can be merged in the model *)
 
-type view_as_cc = Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
+type view_as_cc = Term.t -> (Const.t, Term.t, Term.t list) CC_view.t
 
 (** Arguments to a congruence closure's implementation *)
 module type ARG = sig
@@ -275,7 +275,6 @@ module type BUILD = sig
 end
 
 module Make (_ : ARG) : BUILD
-module Default : BUILD
 
 val create :
   (module ARG) ->
@@ -291,6 +290,10 @@ val create :
       as well.
   *)
 
+val create_default :
+  ?stat:Stat.t -> ?size:[ `Small | `Big ] -> Term.store -> Proof_trace.t -> t
+(** Same as {!create} but with the default CC view *)
+
 (**/**)
 
 module Debug_ : sig
diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index ad7dc973..49cb02fe 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -1,4 +1,3 @@
-open Sidekick_core
 module View = View
 module E_node = E_node
 module Expl = Expl
diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli
index 0facab95..9d2e149e 100644
--- a/src/cc/Sidekick_cc.mli
+++ b/src/cc/Sidekick_cc.mli
@@ -1,7 +1,5 @@
 (** Congruence Closure Implementation *)
 
-open Sidekick_core
-
 module type DYN_MONOID_PLUGIN = Sigs_plugin.DYN_MONOID_PLUGIN
 module type MONOID_PLUGIN_ARG = Sigs_plugin.MONOID_PLUGIN_ARG
 module type MONOID_PLUGIN_BUILDER = Sigs_plugin.MONOID_PLUGIN_BUILDER
diff --git a/src/cc/mini/Sidekick_mini_cc.ml b/src/cc/mini/Sidekick_mini_cc.ml
deleted file mode 100644
index 059ad1b5..00000000
--- a/src/cc/mini/Sidekick_mini_cc.ml
+++ /dev/null
@@ -1,337 +0,0 @@
-open Sidekick_core
-module CC_view = Sidekick_cc.View
-
-module type ARG = sig
-  val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) CC_view.t
-end
-
-module type S = sig
-  type t
-
-  val create : Term.store -> t
-  val clear : t -> unit
-  val add_lit : t -> Term.t -> bool -> unit
-  val check_sat : t -> bool
-  val classes : t -> Term.t Iter.t Iter.t
-end
-
-module Make (A : ARG) = struct
-  open CC_view
-  module T = Term
-  module T_tbl = Term.Tbl
-
-  type node = {
-    n_t: Term.t;
-    mutable n_next: node; (* next in class *)
-    mutable n_size: int; (* size of class *)
-    mutable n_parents: node list;
-    mutable n_root: node; (* root of the class *)
-  }
-
-  type signature = (Const.t, node, node list) CC_view.t
-
-  module Node = struct
-    type t = node
-
-    let[@inline] equal (n1 : t) n2 = T.equal n1.n_t n2.n_t
-    let[@inline] hash (n : t) = T.hash n.n_t
-    let[@inline] size (n : t) = n.n_size
-    let[@inline] is_root n = n == n.n_root
-    let[@inline] root n = n.n_root
-    let[@inline] term n = n.n_t
-    let pp out n = T.pp_debug out n.n_t
-    let add_parent (self : t) ~p : unit = self.n_parents <- p :: self.n_parents
-
-    let make (t : T.t) : t =
-      let rec n =
-        { n_t = t; n_size = 1; n_next = n; n_parents = []; n_root = n }
-      in
-      n
-
-    (* iterate over the class *)
-    let iter_cls (n0 : t) f : unit =
-      let rec aux n =
-        f n;
-        let n' = n.n_next in
-        if equal n' n0 then
-          ()
-        else
-          aux n'
-      in
-      aux n0
-  end
-
-  module Signature = struct
-    type t = signature
-
-    let equal (s1 : t) s2 : bool =
-      match s1, s2 with
-      | Bool b1, Bool b2 -> b1 = b2
-      | App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2
-      | App_fun (f1, l1), App_fun (f2, l2) ->
-        Const.equal f1 f2 && CCList.equal Node.equal l1 l2
-      | App_ho (f1, a1), App_ho (f2, a2) -> Node.equal f1 f2 && Node.equal a1 a2
-      | Not n1, Not n2 -> Node.equal n1 n2
-      | If (a1, b1, c1), If (a2, b2, c2) ->
-        Node.equal a1 a2 && Node.equal b1 b2 && Node.equal c1 c2
-      | Eq (a1, b1), Eq (a2, b2) -> Node.equal a1 a2 && Node.equal b1 b2
-      | Opaque u1, Opaque u2 -> Node.equal u1 u2
-      | Bool _, _
-      | App_fun _, _
-      | App_ho _, _
-      | If _, _
-      | Eq _, _
-      | Opaque _, _
-      | Not _, _ ->
-        false
-
-    let hash (s : t) : int =
-      let module H = CCHash in
-      match s with
-      | Bool b -> H.combine2 10 (H.bool b)
-      | App_fun (f, l) -> H.combine3 20 (Const.hash f) (H.list Node.hash l)
-      | App_ho (f, a) -> H.combine3 30 (Node.hash f) (Node.hash a)
-      | Eq (a, b) -> H.combine3 40 (Node.hash a) (Node.hash b)
-      | Opaque u -> H.combine2 50 (Node.hash u)
-      | If (a, b, c) -> H.combine4 60 (Node.hash a) (Node.hash b) (Node.hash c)
-      | Not u -> H.combine2 70 (Node.hash u)
-
-    let pp out = function
-      | Bool b -> Fmt.bool out b
-      | App_fun (f, []) -> Const.pp out f
-      | App_fun (f, l) ->
-        Fmt.fprintf out "(@[%a@ %a@])" Const.pp f (Util.pp_list Node.pp) l
-      | App_ho (f, a) -> Fmt.fprintf out "(@[%a@ %a@])" Node.pp f Node.pp a
-      | Opaque t -> Node.pp out t
-      | Not u -> Fmt.fprintf out "(@[not@ %a@])" Node.pp u
-      | Eq (a, b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" Node.pp a Node.pp b
-      | If (a, b, c) ->
-        Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" Node.pp a Node.pp b Node.pp c
-  end
-
-  module Sig_tbl = CCHashtbl.Make (Signature)
-
-  type t = {
-    mutable ok: bool; (* unsat? *)
-    tbl: node T_tbl.t;
-    sig_tbl: node Sig_tbl.t;
-    mutable combine: (node * node) list;
-    mutable pending: node list; (* refresh signature *)
-    true_: node;
-    false_: node;
-  }
-
-  let create tst : t =
-    let true_ = Term.true_ tst in
-    let false_ = Term.false_ tst in
-    let self =
-      {
-        ok = true;
-        tbl = T_tbl.create 128;
-        sig_tbl = Sig_tbl.create 128;
-        combine = [];
-        pending = [];
-        true_ = Node.make true_;
-        false_ = Node.make false_;
-      }
-    in
-    T_tbl.add self.tbl true_ self.true_;
-    T_tbl.add self.tbl false_ self.false_;
-    self
-
-  let clear (self : t) : unit =
-    let { ok = _; tbl; sig_tbl; pending = _; combine = _; true_; false_ } =
-      self
-    in
-    self.ok <- true;
-    self.pending <- [];
-    self.combine <- [];
-    T_tbl.clear tbl;
-    Sig_tbl.clear sig_tbl;
-    T_tbl.add tbl true_.n_t true_;
-    T_tbl.add tbl false_.n_t false_;
-    ()
-
-  let sub_ t k : unit =
-    match A.view_as_cc t with
-    | Bool _ | Opaque _ -> ()
-    | App_fun (_, args) -> args k
-    | App_ho (f, a) ->
-      k f;
-      k a
-    | Eq (a, b) ->
-      k a;
-      k b
-    | Not u -> k u
-    | If (a, b, c) ->
-      k a;
-      k b;
-      k c
-
-  let rec add_t (self : t) (t : Term.t) : node =
-    match T_tbl.find self.tbl t with
-    | n -> n
-    | exception Not_found ->
-      let node = Node.make t in
-      T_tbl.add self.tbl t node;
-      (* add sub-terms, and add [t] to their parent list *)
-      sub_ t (fun u ->
-          let n_u = Node.root @@ add_t self u in
-          Node.add_parent n_u ~p:node);
-      (* need to compute signature *)
-      self.pending <- node :: self.pending;
-      node
-
-  let find_t_ (self : t) (t : Term.t) : node =
-    try T_tbl.find self.tbl t |> Node.root
-    with Not_found ->
-      Error.errorf "mini-cc.find_t: no node for %a" T.pp_debug t
-
-  exception E_unsat
-
-  let compute_sig (self : t) (n : node) : Signature.t option =
-    let[@inline] return x = Some x in
-    match A.view_as_cc n.n_t with
-    | Bool _ | Opaque _ -> None
-    | Eq (a, b) ->
-      let a = find_t_ self a in
-      let b = find_t_ self b in
-      return @@ Eq (a, b)
-    | Not u -> return @@ Not (find_t_ self u)
-    | App_fun (f, args) ->
-      let args = args |> Iter.map (find_t_ self) |> Iter.to_list in
-      if args <> [] then
-        return @@ App_fun (f, args)
-      else
-        None
-    | App_ho (f, a) ->
-      let f = find_t_ self f in
-      let a = find_t_ self a in
-      return @@ App_ho (f, a)
-    | If (a, b, c) ->
-      return @@ If (find_t_ self a, find_t_ self b, find_t_ self c)
-
-  let update_sig_ (self : t) (n : node) : unit =
-    match compute_sig self n with
-    | None -> ()
-    | Some (Eq (a, b)) ->
-      if Node.equal a b then (
-        (* reduce to [true] *)
-        let n2 = self.true_ in
-        Log.debugf 5 (fun k ->
-            k "(@[mini-cc.congruence-by-eq@ %a@ %a@])" Node.pp n Node.pp n2);
-        self.combine <- (n, n2) :: self.combine
-      )
-    | Some (Not u) when Node.equal u self.true_ ->
-      self.combine <- (n, self.false_) :: self.combine
-    | Some (Not u) when Node.equal u self.false_ ->
-      self.combine <- (n, self.true_) :: self.combine
-    | Some (If (a, b, _)) when Node.equal a self.true_ ->
-      self.combine <- (n, b) :: self.combine
-    | Some (If (a, _, c)) when Node.equal a self.false_ ->
-      self.combine <- (n, c) :: self.combine
-    | Some s ->
-      Log.debugf 5 (fun k -> k "(@[mini-cc.update-sig@ %a@])" Signature.pp s);
-      (match Sig_tbl.find self.sig_tbl s with
-      | n2 when Node.equal n n2 -> ()
-      | n2 ->
-        (* collision, merge *)
-        Log.debugf 5 (fun k ->
-            k "(@[mini-cc.congruence-by-sig@ %a@ %a@])" Node.pp n Node.pp n2);
-        self.combine <- (n, n2) :: self.combine
-      | exception Not_found -> Sig_tbl.add self.sig_tbl s n)
-
-  let[@inline] is_bool self n =
-    Node.equal self.true_ n || Node.equal self.false_ n
-
-  (* merge the two classes *)
-  let merge_ self n1 n2 : unit =
-    let n1 = Node.root n1 in
-    let n2 = Node.root n2 in
-    if not @@ Node.equal n1 n2 then (
-      (* merge into largest class, or into a boolean *)
-      let n1, n2 =
-        if is_bool self n1 then
-          n1, n2
-        else if is_bool self n2 then
-          n2, n1
-        else if Node.size n1 > Node.size n2 then
-          n1, n2
-        else
-          n2, n1
-      in
-      Log.debugf 5 (fun k ->
-          k "(@[mini-cc.merge@ :into %a@ %a@])" Node.pp n1 Node.pp n2);
-
-      if is_bool self n1 && is_bool self n2 then (
-        Log.debugf 5 (fun k -> k "(mini-cc.conflict.merge-true-false)");
-        self.ok <- false;
-        raise E_unsat
-      );
-
-      self.pending <- List.rev_append n2.n_parents self.pending;
-
-      (* will change signature *)
-
-      (* merge parent lists *)
-      n1.n_parents <- List.rev_append n2.n_parents n1.n_parents;
-      n1.n_size <- n2.n_size + n1.n_size;
-
-      (* update root pointer in [n2.class] *)
-      Node.iter_cls n2 (fun n -> n.n_root <- n1);
-
-      (* merge classes [next] pointers *)
-      let n1_next = n1.n_next in
-      n1.n_next <- n2.n_next;
-      n2.n_next <- n1_next
-    )
-
-  let[@inline] check_ok_ self = if not self.ok then raise_notrace E_unsat
-
-  (* fixpoint of the congruence closure *)
-  let fixpoint (self : t) : unit =
-    while not (CCList.is_empty self.pending && CCList.is_empty self.combine) do
-      check_ok_ self;
-      while not @@ CCList.is_empty self.pending do
-        let n = List.hd self.pending in
-        self.pending <- List.tl self.pending;
-        update_sig_ self n
-      done;
-      while not @@ CCList.is_empty self.combine do
-        let n1, n2 = List.hd self.combine in
-        self.combine <- List.tl self.combine;
-        merge_ self n1 n2
-      done
-    done
-
-  (* API *)
-
-  let add_lit (self : t) (p : T.t) (sign : bool) : unit =
-    match A.view_as_cc p with
-    | Eq (t1, t2) when sign ->
-      let n1 = add_t self t1 in
-      let n2 = add_t self t2 in
-      self.combine <- (n1, n2) :: self.combine
-    | _ ->
-      (* just merge with true/false *)
-      let n = add_t self p in
-      let n2 =
-        if sign then
-          self.true_
-        else
-          self.false_
-      in
-      self.combine <- (n, n2) :: self.combine
-
-  let check_sat (self : t) : bool =
-    try
-      fixpoint self;
-      true
-    with E_unsat ->
-      self.ok <- false;
-      false
-
-  let classes self : _ Iter.t =
-    T_tbl.values self.tbl |> Iter.filter Node.is_root
-    |> Iter.map (fun n -> Node.iter_cls n |> Iter.map Node.term)
-end
diff --git a/src/cc/mini/Sidekick_mini_cc.mli b/src/cc/mini/Sidekick_mini_cc.mli
deleted file mode 100644
index fd4b4493..00000000
--- a/src/cc/mini/Sidekick_mini_cc.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(** Mini congruence closure
-
-    This implementation is as simple as possible, and doesn't provide
-    backtracking, theories, or explanations.
-    It just decides the satisfiability of a set of (dis)equations.
-*)
-
-open Sidekick_core
-module CC_view = Sidekick_cc.View
-
-(** Argument for the functor {!Make}
-
-    It only requires a Term.t structure, and a congruence-oriented view. *)
-module type ARG = sig
-  val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) CC_view.t
-end
-
-(** Main signature for an instance of the mini congruence closure *)
-module type S = sig
-  type t
-  (** An instance of the congruence closure. Mutable *)
-
-  val create : Term.store -> t
-  (** New instance *)
-
-  val clear : t -> unit
-  (** Fully reset the congruence closure's state *)
-
-  val add_lit : t -> Term.t -> bool -> unit
-  (** [add_lit cc p sign] asserts that [p] is true if [sign],
-      or [p] is false if [not sign]. If [p] is an equation and [sign]
-      is [true], this adds a new equation to the congruence relation. *)
-
-  val check_sat : t -> bool
-  (** [check_sat cc] returns [true] if the current state is satisfiable, [false]
-      if it's unsatisfiable. *)
-
-  val classes : t -> Term.t Iter.t Iter.t
-  (** Traverse the set of classes in the congruence closure.
-      This should be called only if {!check} returned [Sat]. *)
-end
-
-(** Instantiate the congruence closure for the given Term.t structure. *)
-module Make (_ : ARG) : S
diff --git a/src/cc/mini/dune b/src/cc/mini/dune
deleted file mode 100644
index 23187086..00000000
--- a/src/cc/mini/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name Sidekick_mini_cc)
- (public_name sidekick.mini-cc)
- (libraries containers iter sidekick.cc sidekick.core sidekick.util)
- (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))
diff --git a/src/cc/mini/tests/dune b/src/cc/mini/tests/dune
deleted file mode 100644
index dfcb4819..00000000
--- a/src/cc/mini/tests/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(library
- (name sidekick_test_minicc)
- (libraries sidekick.mini-cc sidekick-base alcotest)
- (flags :standard -warn-error -a+8))
diff --git a/src/cc/mini/tests/sidekick_test_minicc.ml b/src/cc/mini/tests/sidekick_test_minicc.ml
deleted file mode 100644
index 1a3969bb..00000000
--- a/src/cc/mini/tests/sidekick_test_minicc.ml
+++ /dev/null
@@ -1,179 +0,0 @@
-open! Sidekick_base
-module A = Alcotest
-
-module CC = Sidekick_mini_cc.Make (struct
-  module T = Sidekick_base.Solver_arg
-
-  let view_as_cc = Term.cc_view
-end)
-
-module Setup () = struct
-  let tst = Term.create ()
-  let ( @-> ) l ret = Ty.Fun.mk l ret
-  let ty_i = Ty.atomic_uninterpreted (ID.make "$i")
-  let ty_bool = Ty.bool ()
-  let fun_f = Fun.mk_undef (ID.make "f") ([ ty_i ] @-> ty_i)
-  let fun_g = Fun.mk_undef (ID.make "g") ([ ty_i; ty_i ] @-> ty_i)
-  let fun_p = Fun.mk_undef (ID.make "p") ([ ty_i ] @-> ty_bool)
-  let fun_a = Fun.mk_undef_const (ID.make "a") ty_i
-  let fun_b = Fun.mk_undef_const (ID.make "b") ty_i
-  let fun_c = Fun.mk_undef_const (ID.make "c") ty_i
-  let fun_d1 = Fun.mk_undef_const (ID.make "d1") ty_i
-  let fun_d2 = Fun.mk_undef_const (ID.make "d2") ty_i
-  let true_ = Term.true_ tst
-  let false_ = Term.false_ tst
-  let const c = Term.const tst c
-  let app_a f l = Term.app_fun tst f l
-  let app_l f l = Term.app_fun tst f (CCArray.of_list l)
-  let not_ x = Term.not_ tst x
-  let eq a b = Term.eq tst a b
-  let neq a b = Term.not_ tst (eq a b)
-  let ite a b c = Term.ite tst a b c
-  let a = const fun_a
-  let b = const fun_b
-  let c = const fun_c
-  let d1 = const fun_d1
-  let d2 = const fun_d2
-  let f t1 = app_l fun_f [ t1 ]
-  let g t1 t2 = app_l fun_g [ t1; t2 ]
-  let p t1 = app_l fun_p [ t1 ]
-end
-
-let l : unit Alcotest.test_case list ref = ref []
-let mk_test name f = l := (name, `Quick, f) :: !l
-
-let () =
-  mk_test "test_p_a_b" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.(p a) true;
-  CC.add_lit cc S.(p b) false;
-  A.(check bool) "is-sat" (CC.check_sat cc) true;
-  CC.add_lit cc S.(eq a b) true;
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let () =
-  mk_test "test_p_a_b_2" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.(p a) true;
-  CC.add_lit cc S.(not_ @@ p b) true;
-  A.(check bool) "is-sat" (CC.check_sat cc) true;
-  CC.add_lit cc S.(eq a b) true;
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let () =
-  mk_test "test_f_f_f_a" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.(neq a (f (f (f (f (f (f a))))))) true;
-  A.(check bool) "is-sat" (CC.check_sat cc) true;
-  CC.add_lit cc S.(eq a (f a)) true;
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let () =
-  mk_test "test_repeated_f_f_f_a" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  for _i = 0 to 10 do
-    CC.add_lit cc S.(neq a (f (f (f (f (f (f a))))))) true;
-    A.(check bool) "is-sat" (CC.check_sat cc) true;
-    CC.add_lit cc S.(eq a (f a)) true;
-    A.(check bool) "is-unsat" (CC.check_sat cc) false;
-    CC.clear cc
-  done;
-  ()
-
-let () =
-  mk_test "test_trans" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.(eq a b) true;
-  CC.add_lit cc S.(eq b c) true;
-  A.(check bool) "is-sat" (CC.check_sat cc) true;
-  CC.add_lit cc S.(neq (f a) (f c)) true;
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let () =
-  mk_test "test_true" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.true_ true;
-  A.(check bool) "is-sat" (CC.check_sat cc) true;
-  CC.add_lit cc S.false_ true;
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let () =
-  mk_test "test_repeated_true" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  for _i = 0 to 10 do
-    CC.add_lit cc S.true_ true;
-    A.(check bool) "is-sat" (CC.check_sat cc) true;
-    CC.add_lit cc S.false_ true;
-    A.(check bool) "is-unsat" (CC.check_sat cc) false;
-    CC.clear cc
-  done;
-  ()
-
-let () =
-  mk_test "test_false" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.false_ true;
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let () =
-  mk_test "test_not_false" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.(not_ false_) true;
-  A.(check bool) "is-sat" (CC.check_sat cc) true;
-  ()
-
-let () =
-  mk_test "test_ite" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  for _i = 0 to 10 do
-    CC.add_lit cc S.(eq a b) true;
-    CC.add_lit cc S.(p (ite (eq a c) d1 d2)) true;
-    CC.add_lit cc S.(not_ (p d1)) true;
-    CC.add_lit cc S.(p d2) true;
-    A.(check bool) "is-sat" (CC.check_sat cc) true;
-    CC.add_lit cc S.(eq b c) true;
-    (* force (p d1) *)
-    A.(check bool) "is-unsat" (CC.check_sat cc) false;
-    CC.clear cc
-  done;
-  ()
-
-(* from the following PO:
-    `cl (- a = (g a c)),
-        (- b = (g a c)),
-        (- c = (g c b)),
-        (- a = (g c c)),
-        (- (g c (g c b)) = (g (g c c) b)),
-        (+ (g a b) = (g a c))))`
-*)
-let () =
-  mk_test "test_reg_1" @@ fun () ->
-  let module S = Setup () in
-  let cc = CC.create S.tst in
-  CC.add_lit cc S.(eq a (g a c)) true;
-  CC.add_lit cc S.(eq b (g a c)) true;
-  CC.add_lit cc S.(eq c (g c b)) true;
-  CC.add_lit cc S.(eq a (g c c)) true;
-  CC.add_lit cc S.(eq (g c (g c b)) (g (g c c) b)) true;
-  CC.add_lit cc S.(eq (g a b) (g a c)) false;
-  (* goal *)
-  A.(check bool) "is-unsat" (CC.check_sat cc) false;
-  ()
-
-let tests = "mini-cc", List.rev !l
diff --git a/src/cc/signature.ml b/src/cc/signature.ml
index 8fdc5ee7..fa1adf7c 100644
--- a/src/cc/signature.ml
+++ b/src/cc/signature.ml
@@ -1,13 +1,13 @@
 (** A signature is a shallow term shape where immediate subterms
       are representative *)
 
-open View
+open Sidekick_core.CC_view
 open Types_
 
 type t = signature
 
 let equal (s1 : t) s2 : bool =
-  let open View in
+  let open CC_view in
   match s1, s2 with
   | Bool b1, Bool b2 -> b1 = b2
   | App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2
diff --git a/src/cc/types_.ml b/src/cc/types_.ml
index c1e1bae1..86fba51b 100644
--- a/src/cc/types_.ml
+++ b/src/cc/types_.ml
@@ -18,7 +18,7 @@ type e_node = {
       An equivalence class is represented by its "root" element,
       the representative. *)
 
-and signature = (Const.t, e_node, e_node list) View.t
+and signature = (Const.t, e_node, e_node list) CC_view.t
 
 and explanation_forest_link =
   | FL_none
diff --git a/src/cc/view.ml b/src/cc/view.ml
index e319f5ef..e69de29b 100644
--- a/src/cc/view.ml
+++ b/src/cc/view.ml
@@ -1,38 +0,0 @@
-type ('f, 't, 'ts) t =
-  | Bool of bool
-  | App_fun of 'f * 'ts
-  | App_ho of 't * 't
-  | If of 't * 't * 't
-  | Eq of 't * 't
-  | Not of 't
-  | Opaque of 't
-(* do not enter *)
-
-let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
-  match v with
-  | Bool b -> Bool b
-  | App_fun (f, args) -> App_fun (f_f f, f_ts args)
-  | App_ho (f, a) -> App_ho (f_t f, f_t a)
-  | Not t -> Not (f_t t)
-  | If (a, b, c) -> If (f_t a, f_t b, f_t c)
-  | Eq (a, b) -> Eq (f_t a, f_t b)
-  | Opaque t -> Opaque (f_t t)
-
-let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
-  match v with
-  | Bool _ -> ()
-  | App_fun (f, args) ->
-    f_f f;
-    f_ts args
-  | App_ho (f, a) ->
-    f_t f;
-    f_t a
-  | Not t -> f_t t
-  | If (a, b, c) ->
-    f_t a;
-    f_t b;
-    f_t c
-  | Eq (a, b) ->
-    f_t a;
-    f_t b
-  | Opaque t -> f_t t
diff --git a/src/cc/view.mli b/src/cc/view.mli
index 038ea1a6..e69de29b 100644
--- a/src/cc/view.mli
+++ b/src/cc/view.mli
@@ -1,33 +0,0 @@
-(** View terms through the lens of the Congruence Closure *)
-
-(** A view of a term fron the point of view of the congruence closure.
-
-      - ['f] is the type of function symbols
-      - ['t] is the type of terms
-      - ['ts] is the type of sequences of terms (arguments of function application)
-  *)
-type ('f, 't, 'ts) t =
-  | Bool of bool
-  | App_fun of 'f * 'ts
-  | App_ho of 't * 't
-  | If of 't * 't * 't
-  | Eq of 't * 't
-  | Not of 't
-  | Opaque of 't  (** do not enter *)
-
-val map_view :
-  f_f:('a -> 'b) ->
-  f_t:('c -> 'd) ->
-  f_ts:('e -> 'f) ->
-  ('a, 'c, 'e) t ->
-  ('b, 'd, 'f) t
-(** Map function over a view, one level deep.
-    Each function maps over a different type, e.g. [f_t] maps over terms *)
-
-val iter_view :
-  f_f:('a -> unit) ->
-  f_t:('b -> unit) ->
-  f_ts:('c -> unit) ->
-  ('a, 'b, 'c) t ->
-  unit
-(** Iterate over a view, one level deep. *)