diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 70c34a6c40dc41f6f22027b1bf430e8fbb41724b..fe6ecdde6a38e8fc7ac3090adad45090218551de 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -200,10 +200,9 @@ let apply_const v = apply_cst Builtin.array_const [] [ v ]
 let apply_def_index a = apply_cst Builtin.array_default_index [] [ a ]
 let apply_def_value a = apply_cst Builtin.array_default_value [] [ a ]
 
-let eq_array_diff a b =
-  Expr.Term.eq
-    (Expr.Term.Array.select a (apply_cst Builtin.array_diff [] [ a; b ]))
-    (Expr.Term.Array.select b (apply_cst Builtin.array_diff [] [ a; b ]))
+let distinct_arrays a b =
+  let diff = apply_diff a b in
+  Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
 
 let apply_ext env a b =
   let va = Expr.Term.Var.mk "a" array_ty in
@@ -378,7 +377,7 @@ module Theory = struct
       | (nvar, nterm, nnode) :: t ->
           let nterms =
             List.fold_left
-              (fun acc (_, oterm, _) -> eq_array_diff nterm oterm :: acc)
+              (fun acc (_, oterm, _) -> distinct_arrays nterm oterm :: acc)
               [] t
           in
           aux (nterms @ terms_acc) ((nvar, nnode) :: tsubsts_acc) t
@@ -404,7 +403,7 @@ module Theory = struct
                       Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt
                     in
                     let anvt = Expr.Term.of_var anv in
-                    ( eq_array_diff a0vt anvt :: nterms,
+                    ( distinct_arrays a0vt anvt :: nterms,
                       (anv, anvt, node) :: nsubsts,
                       cnt + 1 ))
                   ([], [], 1) t