diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 28819685017c8cf8e5f08cf037aa04819d409297..55457fbb69c270e7b8fe8796425d17f423cc6bb6 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -22,10 +22,6 @@
 open Colibri2_core
 open Colibri2_popop_lib
 
-(*
-
-*)
-
 let db = Datastructure.Push.create Ground.pp "Array.db"
 let debug = Debug.register_info_flag ~desc:"For array theory" "Array"
 let stats = Debug.register_stats_int "Array.rule"
@@ -34,7 +30,10 @@ let convert ~subst =
   Colibri2_theories_quantifiers.Subst.convert ~subst_old:Ground.Subst.empty
     ~subst_new:subst
 
-module Select_store = struct
+(* Generalized, Efficient Array Decision Procedures. de Moura, Bjorner *)
+module Theory = struct
+  open Colibri2_theories_quantifiers
+
   let term_of_var = Expr.Term.of_var
   let mk_int_var name = Expr.Term.Var.mk name Expr.Ty.int
 
@@ -56,23 +55,19 @@ module Select_store = struct
   let ta = term_of_var va
   let tb = term_of_var vb
 
-  open Colibri2_theories_quantifiers
-
-  (* n ≡ b[i <- v] |> n[i] = v *)
-  let idx_pattern, idx_run =
-    let term = Expr.Term.store tb ti tv in
-    let idx_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
-    let idx_run env subst =
-      Debug.dprintf2 debug "Found idx with %a" Ground.Subst.pp subst;
-      let v = Expr.Term.Var.M.find_exn Impossible vv subst.term in
-      let n_i = convert ~subst env @@ Expr.Term.select term ti in
-      Egraph.register env n_i;
-      Egraph.register env v;
-      Egraph.merge env n_i v
-    in
-    (idx_pattern, idx_run)
+  let distinct_term =
+    Expr.Term._or
+      [
+        Expr.Term.eq ta tb;
+        (let kab_v = Expr.Term.Var.mk "k_a_b" Expr.Ty.int in
+         let kab_t = Expr.Term.of_var kab_v in
+         Expr.Term.ex ([], [ kab_v ])
+         @@ Expr.Term.neq
+              (Expr.Term.select ta kab_t)
+              (Expr.Term.select tb kab_t));
+      ]
 
-  (* a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
+  (* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
   let adown_pattern, adown_run =
     let a = Expr.Term.store tb ti tv in
     let term = Expr.Term.select a tj in
@@ -94,7 +89,7 @@ module Select_store = struct
     in
     (adown_pattern, adown_run)
 
-  (* a ≡ b[i <- v], b[j]  |> (i = j) \/ a[j] = b[j] *)
+  (* ⇑: a ≡ b[i <- v], b[j]  |> (i = j) \/ a[j] = b[j] *)
   let aup_pattern, aup_run =
     let term = Expr.Term.store tb ti tv in
     let aup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
@@ -104,10 +99,9 @@ module Select_store = struct
       Debug.dprintf2 debug "Found aup1 with %a" Ground.Subst.pp subst;
       let term_bis = Expr.Term.select tb tj in
       let aup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
-      let aup_run_bis env subst2 =
+      let aup_run_bis env subst_bis =
         Debug.incr stats;
-        let subst = Ground.Subst.distinct_union subst2 subst in
-        (* ? *)
+        let subst = Ground.Subst.distinct_union subst_bis subst in
         Debug.dprintf2 debug "Found aup2 with %a" Ground.Subst.pp subst;
         let v =
           convert ~subst env
@@ -128,24 +122,9 @@ module Select_store = struct
   let init env =
     List.iter
       (fun (p, r) -> InvertedPath.add_callback env p r)
-      [
-        (idx_pattern, idx_run);
-        (adown_pattern, adown_run);
-        (aup_pattern, aup_run);
-      ]
-
-  let distinct_term =
-    Expr.Term._or
-      [
-        Expr.Term.eq ta tb;
-        (let kab_v = Expr.Term.Var.mk "k_a_b" Expr.Ty.int in
-         let kab_t = Expr.Term.of_var kab_v in
-         Expr.Term.ex ([], [ kab_v ])
-         @@ Expr.Term.neq
-              (Expr.Term.select ta kab_t)
-              (Expr.Term.select tb kab_t));
-      ]
+      [ (adown_pattern, adown_run); (aup_pattern, aup_run) ]
 
+  (* ext: a, b ⇒ (a = b) ⋁ (a[k] ≠ b[k])   *)
   let new_array env f =
     Datastructure.Push.iter db env ~f:(fun f2 ->
         let subst =
@@ -165,24 +144,44 @@ module Select_store = struct
 end
 
 let converter env (f : Ground.t) =
-  let _r = Ground.node f in
-  (match (Ground.sem f).ty with
-  | { app = { builtin = Expr.Array; _ }; _ } -> Select_store.new_array env f
+  let s = Ground.sem f in
+  (match s.ty with
+  | { app = { builtin = Expr.Array; _ }; _ } -> Theory.new_array env f
   | _ -> ());
-  match Ground.sem f with
-  | { app = { builtin = Expr.Select; _ }; args; tyargs = _; _ } ->
+  match s with
+  | { app = { builtin = Expr.Select; _ }; args; _ } ->
       let a, k = IArray.extract2_exn args in
       Egraph.register env a;
       Egraph.register env k
-  | { app = { builtin = Expr.Store; _ }; args; tyargs = _; _ } ->
+  | { app = { builtin = Expr.Store; _ }; args; _ } ->
       let a, k, v = IArray.extract3_exn args in
       Egraph.register env a;
       Egraph.register env k;
-      Egraph.register env v
+      Egraph.register env v;
+      (* application of the `idx` rule *)
+      let subst =
+        Ground.Subst.
+          {
+            term =
+              Expr.Term.Var.M.of_list
+                [ (Theory.va, a); (Theory.vk, k); (Theory.vv, v) ];
+            ty = Expr.Ty.Var.M.empty;
+          }
+      in
+      let rn =
+        convert ~subst env
+          (Expr.Term.eq
+             (Expr.Term.select
+                (Expr.Term.store Theory.ta Theory.tk Theory.tv)
+                Theory.tk)
+             Theory.tv)
+      in
+      Egraph.register env rn;
+      Boolean.set_true env rn
   | _ -> ()
 
 let init env : unit =
   Ground.register_converter env converter;
-  Select_store.init env
+  Theory.init env
 
 let () = Init.add_default_theory init