diff --git a/regression/test001.t b/regression/test001.t
index 3c9ce3cc..43e31c8e 100644
--- a/regression/test001.t
+++ b/regression/test001.t
@@ -69,20 +69,20 @@
   fun q -> reverso q q, 3 answers {
   q=[];
   q=[_.11];
-  q=[_.23; _.23];
+  q=[_.11; _.11];
   }
   fun q -> reverso q q, 10 answers {
   q=[];
   q=[_.11];
-  q=[_.23; _.23];
-  q=[_.56; _.32; _.56];
-  q=[_.110; _.89; _.89; _.110];
-  q=[_.188; _.167; _.134; _.167; _.188];
-  q=[_.293; _.266; _.236; _.236; _.266; _.293];
-  q=[_.422; _.398; _.365; _.329; _.365; _.398; _.422];
-  q=[_.578; _.554; _.524; _.488; _.488; _.524; _.554; _.578];
-  q=[_.770; _.743; _.713; _.683; _.638; _.683; _.713; _.743; _.770];
+  q=[_.11; _.11];
+  q=[_.11; _.20; _.11];
+  q=[_.11; _.20; _.20; _.11];
+  q=[_.11; _.20; _.26; _.20; _.11];
+  q=[_.11; _.20; _.26; _.26; _.20; _.11];
+  q=[_.11; _.20; _.26; _.38; _.26; _.20; _.11];
+  q=[_.11; _.20; _.26; _.38; _.38; _.26; _.20; _.11];
+  q=[_.11; _.20; _.26; _.38; _.53; _.38; _.26; _.20; _.11];
   }
   fun q r -> two_vars q r, 1 answer {
-  q=_.11; r=_.11;
+  q=_.10; r=_.10;
   }
diff --git a/regression/test002.t b/regression/test002.t
index c3abc17a..58c7a972 100644
--- a/regression/test002.t
+++ b/regression/test002.t
@@ -1,13 +1,13 @@
   $ ./test002sort.exe
-  [O; O; _.138]
-  [O; O; _.136 [=/= O]]
-  [O; O; _.153 [=/= O]]
-  [O; S (O); S (_.497)]
-  [O; S (O); S (_.516 [=/= O])]
+  [O; O; _.12]
+  [O; O; _.11 [=/= O]]
+  [O; O; _.10 [=/= O]]
   [O; S (O); S (_.110)]
+  [O; S (O); S (_.110 [=/= O])]
   [O; S (O); S (_.110)]
-  [S (O); S (O); S (_.781)]
-  [S (O); S (O); S (_.804 [=/= O])]
+  [O; S (O); S (_.110)]
+  [S (O); S (O); S (_.110)]
+  [S (O); S (O); S (_.110 [=/= O])]
   [O; S (O); S (_.160 [=/= O])]
   []
   
diff --git a/regression/test005.t b/regression/test005.t
index 85d225fd..0ac2195e 100644
--- a/regression/test005.t
+++ b/regression/test005.t
@@ -19,14 +19,14 @@
   q=[("x", V ("y")) | _.13];
   }
   fun q -> infero (abs varX (v varX)) q, 1 answer {
-  q=Arr (_.18, _.18);
+  q=Arr (_.17, _.17);
   }
   fun q -> infero (abs varF (abs varX (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (Arr (_.30, _.26), Arr (_.30, _.26));
+  q=Arr (Arr (_.25, _.26), Arr (_.25, _.26));
   }
   fun q -> infero (abs varX (abs varF (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (_.30, Arr (Arr (_.30, _.26), _.26));
+  q=Arr (_.17, Arr (Arr (_.17, _.26), _.26));
   }
   fun q -> infero q (arr (p varX) (p varX)), 1 answer {
-  q=Abs (_.29, V (_.29));
+  q=Abs (_.18, V (_.18));
   }
diff --git a/regression/test006.t b/regression/test006.t
index f56d607c..f3734dee 100644
--- a/regression/test006.t
+++ b/regression/test006.t
@@ -24,12 +24,12 @@
   q=V ("x");
   }
   fun q -> evalo (app q (v varX)) (v varX), 1 answer {
-  q=Abs (_.44, V (_.44));
+  q=Abs (_.19, V (_.19));
   }
   fun q r -> evalo (app r q) (v varX), 1 answer {
-  q=V ("x"); r=Abs (_.54, V (_.54));
+  q=V ("x"); r=Abs (_.20, V (_.20));
   }
   fun q r s -> a_la_quine q r s, 2 answers {
-  q=Abs (_.668, V (_.668)); r=Abs (_.668, V (_.668)); s=Abs (_.668, V (_.668));
-  q=Abs (_.783, V (_.783)); r=Abs (_.783, Abs (_.783, V (_.783))); s=Abs (_.783, Abs (_.783, V (_.783)));
+  q=Abs (_.21, V (_.21)); r=Abs (_.21, V (_.21)); s=Abs (_.21, V (_.21));
+  q=Abs (_.21, V (_.21)); r=Abs (_.21, Abs (_.21, V (_.21))); s=Abs (_.21, Abs (_.21, V (_.21)));
   }
diff --git a/regression/test007.t b/regression/test007.t
index 4738cf14..ebb46803 100644
--- a/regression/test007.t
+++ b/regression/test007.t
@@ -24,8 +24,8 @@
   q=V ("x");
   }
   fun q -> evalo (app q (v varX)) (v varX), 1 answer {
-  q=Abs (_.39, V (_.39));
+  q=Abs (_.21, V (_.21));
   }
   fun q r -> evalo (app r q) (v varX), 1 answer {
-  q=V ("x"); r=Abs (_.40, V (_.40));
+  q=V ("x"); r=Abs (_.22, V (_.22));
   }
diff --git a/regression/test010.t b/regression/test010.t
index f637ce50..88db7b3c 100644
--- a/regression/test010.t
+++ b/regression/test010.t
@@ -86,7 +86,7 @@
   fun q -> (q === !3) &&& (!3 =/= q), all answers {
   }
   fun q r -> (q =/= !!(true)) &&& (q =/= r), all answers {
-  q=_.10 [=/= _.11; =/= true]; r=_.11;
+  q=_.10 [=/= true]; r=_.11 [=/= _.10 [=/= true]];
   }
   fun q -> q =/= Std.nil (), all answers {
   q=_.10 [=/= []];
diff --git a/regression/test011.t b/regression/test011.t
index a4a7a153..14406416 100644
--- a/regression/test011.t
+++ b/regression/test011.t
@@ -162,7 +162,7 @@
   fun q ->
     OCanren.Fresh.two
       (fun x y -> delay (fun () -> conj (!![x; y] === q) (x =/= y))), all answers {
-  q=[_.11 [=/= _.12]; _.12];
+  q=[_.11; _.12 [=/= _.11]];
   }
   fun q -> Fresh.two (fun a d -> ?&[!![a; d] === q; q =/= !![!5; !6]]), all answers {
   q=[_.11; _.12 [=/= 6]];
@@ -180,13 +180,13 @@
     OCanren.Fresh.two
       (fun x y ->
          delay (fun () -> conj (conj (!![x; y] === q) (x =/= y)) (y =/= x))), all answers {
-  q=[_.11 [=/= _.12]; _.12];
+  q=[_.11; _.12 [=/= _.11]];
   }
   fun q ->
     OCanren.Fresh.two
       (fun x y ->
          delay (fun () -> conj (conj (!![x; y] === q) (x =/= y)) (x =/= y))), all answers {
-  q=[_.11 [=/= _.12]; _.12];
+  q=[_.11; _.12 [=/= _.11]];
   }
   fun q -> (q =/= !5) &&& (!5 =/= q), all answers {
   q=_.10 [=/= 5];
@@ -250,7 +250,7 @@
   q=[_.12 [=/= _.11]; 2];
   }
   fun q -> distincto (!2 % (!3 %< q)), all answers {
-  q=_.35 [=/= 2; =/= 3];
+  q=_.10 [=/= 2; =/= 3];
   }
   fun q -> remembero !1 (!1 % (!2 % (!1 %< !3))) q, all answers {
   q=[2; 3];
diff --git a/regression/test014.t b/regression/test014.t
index c1f784a2..7ea9923e 100644
--- a/regression/test014.t
+++ b/regression/test014.t
@@ -1,26 +1,26 @@
   $ ./test014.exe
   fun q r s -> pluso q r s, 22 answers {
-  q=_.12; r=[]; s=_.12;
+  q=_.10; r=[]; s=_.10;
   q=[]; r=[_.13 | _.14]; s=[_.13 | _.14];
   q=[1]; r=[1]; s=[0; 1];
-  q=[1]; r=[0; _.46 | _.47]; s=[1; _.46 | _.47];
+  q=[1]; r=[0; _.27 | _.28]; s=[1; _.27 | _.28];
   q=[1]; r=[1; 1]; s=[0; 0; 1];
-  q=[0; _.109 | _.110]; r=[1]; s=[1; _.109 | _.110];
+  q=[0; _.25 | _.26]; r=[1]; s=[1; _.25 | _.26];
   q=[0; 1]; r=[0; 1]; s=[0; 0; 1];
-  q=[1]; r=[1; 0; _.154 | _.155]; s=[0; 1; _.154 | _.155];
+  q=[1]; r=[1; 0; _.90 | _.91]; s=[0; 1; _.90 | _.91];
   q=[1]; r=[1; 1; 1]; s=[0; 0; 0; 1];
   q=[1; 1]; r=[1]; s=[0; 0; 1];
   q=[1; 1]; r=[0; 1]; s=[1; 0; 1];
-  q=[1]; r=[1; 1; 0; _.286 | _.287]; s=[0; 0; 1; _.286 | _.287];
+  q=[1]; r=[1; 1; 0; _.207 | _.208]; s=[0; 0; 1; _.207 | _.208];
   q=[1]; r=[1; 1; 1; 1]; s=[0; 0; 0; 0; 1];
-  q=[1; 0; _.345 | _.346]; r=[1]; s=[0; 1; _.345 | _.346];
-  q=[1]; r=[1; 1; 1; 0; _.391 | _.392]; s=[0; 0; 0; 1; _.391 | _.392];
+  q=[1; 0; _.210 | _.211]; r=[1]; s=[0; 1; _.210 | _.211];
+  q=[1]; r=[1; 1; 1; 0; _.331 | _.332]; s=[0; 0; 0; 1; _.331 | _.332];
   q=[0; 1]; r=[1; 1]; s=[1; 0; 1];
   q=[1]; r=[1; 1; 1; 1; 1]; s=[0; 0; 0; 0; 0; 1];
   q=[1; 1; 1]; r=[1]; s=[0; 0; 0; 1];
   q=[1; 1]; r=[1; 1]; s=[0; 1; 1];
-  q=[0; 1]; r=[0; 0; _.333 | _.334]; s=[0; 1; _.333 | _.334];
-  q=[1]; r=[1; 1; 1; 1; 0; _.510 | _.511]; s=[0; 0; 0; 0; 1; _.510 | _.511];
+  q=[0; 1]; r=[0; 0; _.161 | _.162]; s=[0; 1; _.161 | _.162];
+  q=[1]; r=[1; 1; 1; 1; 0; _.452 | _.453]; s=[0; 0; 0; 0; 1; _.452 | _.453];
   q=[1]; r=[1; 1; 1; 1; 1; 1]; s=[0; 0; 0; 0; 0; 0; 1];
   }
   fun q r s -> multo q r s, 34 answers {
@@ -29,31 +29,31 @@
   q=[1]; r=[_.15 | _.16]; s=[_.15 | _.16];
   q=[_.17; _.18 | _.19]; r=[1]; s=[_.17; _.18 | _.19];
   q=[0; 1]; r=[_.28; _.33 | _.34]; s=[0; _.28; _.33 | _.34];
-  q=[0; 0; 1]; r=[_.69; _.76 | _.77]; s=[0; 0; _.69; _.76 | _.77];
-  q=[1; _.102 | _.103]; r=[0; 1]; s=[0; 1; _.102 | _.103];
-  q=[0; 0; 0; 1]; r=[_.149; _.164 | _.165]; s=[0; 0; 0; _.149; _.164 | _.165];
-  q=[1; _.192 | _.193]; r=[0; 0; 1]; s=[0; 0; 1; _.192 | _.193];
-  q=[0; 1; _.218 | _.219]; r=[0; 1]; s=[0; 0; 1; _.218 | _.219];
-  q=[0; 0; 0; 0; 1]; r=[_.314; _.343 | _.344]; s=[0; 0; 0; 0; _.314; _.343 | _.344];
-  q=[1; _.375 | _.376]; r=[0; 0; 0; 1]; s=[0; 0; 0; 1; _.375 | _.376];
-  q=[0; 1; _.401 | _.402]; r=[0; 0; 1]; s=[0; 0; 0; 1; _.401 | _.402];
-  q=[0; 0; 1; _.459 | _.460]; r=[0; 1]; s=[0; 0; 0; 1; _.459 | _.460];
+  q=[0; 0; 1]; r=[_.32; _.33 | _.34]; s=[0; 0; _.32; _.33 | _.34];
+  q=[1; _.30 | _.31]; r=[0; 1]; s=[0; 1; _.30 | _.31];
+  q=[0; 0; 0; 1]; r=[_.32; _.33 | _.34]; s=[0; 0; 0; _.32; _.33 | _.34];
+  q=[1; _.30 | _.31]; r=[0; 0; 1]; s=[0; 0; 1; _.30 | _.31];
+  q=[0; 1; _.71 | _.72]; r=[0; 1]; s=[0; 0; 1; _.71 | _.72];
+  q=[0; 0; 0; 0; 1]; r=[_.32; _.33 | _.34]; s=[0; 0; 0; 0; _.32; _.33 | _.34];
+  q=[1; _.30 | _.31]; r=[0; 0; 0; 1]; s=[0; 0; 0; 1; _.30 | _.31];
+  q=[0; 1; _.71 | _.72]; r=[0; 0; 1]; s=[0; 0; 0; 1; _.71 | _.72];
+  q=[0; 0; 1; _.155 | _.156]; r=[0; 1]; s=[0; 0; 0; 1; _.155 | _.156];
   q=[1; 1]; r=[1; 1]; s=[1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 1]; r=[_.656; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.656; _.713 | _.714];
-  q=[1; _.745 | _.746]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.745 | _.746];
-  q=[0; 1; _.778 | _.779]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.778 | _.779];
-  q=[0; 0; 1; _.834 | _.835]; r=[0; 0; 1]; s=[0; 0; 0; 0; 1; _.834 | _.835];
-  q=[0; 0; 0; 1; _.946 | _.947]; r=[0; 1]; s=[0; 0; 0; 0; 1; _.946 | _.947];
+  q=[0; 0; 0; 0; 0; 1]; r=[_.32; _.33 | _.34]; s=[0; 0; 0; 0; 0; _.32; _.33 | _.34];
+  q=[1; _.30 | _.31]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.30 | _.31];
+  q=[0; 1; _.71 | _.72]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.71 | _.72];
+  q=[0; 0; 1; _.155 | _.156]; r=[0; 0; 1]; s=[0; 0; 0; 0; 1; _.155 | _.156];
+  q=[0; 0; 0; 1; _.326 | _.327]; r=[0; 1]; s=[0; 0; 0; 0; 1; _.326 | _.327];
   q=[1; 1]; r=[1; 0; 1]; s=[1; 1; 1; 1];
   q=[0; 1; 1]; r=[1; 1]; s=[0; 1; 0; 0; 1];
   q=[1; 1]; r=[1; 1; 1]; s=[1; 0; 1; 0; 1];
   q=[1; 1]; r=[0; 1; 1]; s=[0; 1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1360; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1360; _.1493 | _.1494];
-  q=[1; _.1523 | _.1524]; r=[0; 0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1523 | _.1524];
-  q=[0; 1; _.1553 | _.1554]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1553 | _.1554];
-  q=[0; 0; 1; _.1607 | _.1608]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1607 | _.1608];
-  q=[0; 0; 0; 1; _.1716 | _.1717]; r=[0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1716 | _.1717];
-  q=[0; 0; 0; 0; 1; _.1946 | _.1947]; r=[0; 1]; s=[0; 0; 0; 0; 0; 1; _.1946 | _.1947];
+  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.32; _.33 | _.34]; s=[0; 0; 0; 0; 0; 0; _.32; _.33 | _.34];
+  q=[1; _.30 | _.31]; r=[0; 0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.30 | _.31];
+  q=[0; 1; _.71 | _.72]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.71 | _.72];
+  q=[0; 0; 1; _.155 | _.156]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.155 | _.156];
+  q=[0; 0; 0; 1; _.326 | _.327]; r=[0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.326 | _.327];
+  q=[0; 0; 0; 0; 1; _.682 | _.683]; r=[0; 1]; s=[0; 0; 0; 0; 0; 1; _.682 | _.683];
   q=[1; 0; 1]; r=[1; 1]; s=[1; 1; 1; 1];
   q=[1; 1]; r=[1; 0; 0; 1]; s=[1; 1; 0; 1; 1];
   q=[0; 1; 1]; r=[1; 0; 1]; s=[0; 1; 1; 1; 1];
@@ -64,11 +64,11 @@
   q=[1]; r=[0; 1];
   q=[0; 1]; r=[0; 0; 1];
   q=[1; 1]; r=[0; 1; 1];
-  q=[1; _.225; 1]; r=[0; 1; _.225; 1];
+  q=[1; _.70; 1]; r=[0; 1; _.70; 1];
   q=[0; 0; 1]; r=[0; 0; 0; 1];
   q=[0; 1; 1]; r=[0; 0; 1; 1];
-  q=[1; _.247; _.408; 1]; r=[0; 1; _.247; _.408; 1];
-  q=[0; 1; _.408; 1]; r=[0; 0; 1; _.408; 1];
+  q=[1; _.70; _.128; 1]; r=[0; 1; _.70; _.128; 1];
+  q=[0; 1; _.128; 1]; r=[0; 0; 1; _.128; 1];
   q=[0; 0; 0; 1]; r=[0; 0; 0; 0; 1];
   }
   fun q r -> lelo q r, 15 answers {
@@ -77,19 +77,19 @@
   q=[]; r=[_.12 | _.13];
   q=[1]; r=[_.14; _.15 | _.16];
   q=[_.17; 1]; r=[_.19; 1];
-  q=[_.23; 1]; r=[_.25; _.39; _.40 | _.41];
-  q=[_.17; _.33; 1]; r=[_.19; _.35; 1];
-  q=[_.17; _.33; _.50; 1]; r=[_.19; _.35; _.52; 1];
-  q=[_.23; _.44; 1]; r=[_.25; _.46; _.60; _.61 | _.62];
-  q=[_.17; _.33; _.50; _.67; 1]; r=[_.19; _.35; _.52; _.69; 1];
-  q=[_.23; _.44; _.63; 1]; r=[_.25; _.46; _.65; _.79; _.80 | _.81];
-  q=[_.17; _.33; _.50; _.67; _.86; 1]; r=[_.19; _.35; _.52; _.69; _.88; 1];
-  q=[_.23; _.44; _.63; _.82; 1]; r=[_.25; _.46; _.65; _.84; _.98; _.99 | _.100];
-  q=[_.17; _.33; _.50; _.67; _.86; _.101; 1]; r=[_.19; _.35; _.52; _.69; _.88; _.103; 1];
-  q=[_.23; _.44; _.63; _.82; _.105; 1]; r=[_.25; _.46; _.65; _.84; _.107; _.121; _.122 | _.123];
+  q=[_.23; 1]; r=[_.25; _.31; _.40 | _.41];
+  q=[_.17; _.21; 1]; r=[_.19; _.27; 1];
+  q=[_.17; _.21; _.37; 1]; r=[_.19; _.27; _.42; 1];
+  q=[_.23; _.29; 1]; r=[_.25; _.31; _.54; _.61 | _.62];
+  q=[_.17; _.21; _.37; _.56; 1]; r=[_.19; _.27; _.42; _.58; 1];
+  q=[_.23; _.29; _.48; 1]; r=[_.25; _.31; _.54; _.75; _.80 | _.81];
+  q=[_.17; _.21; _.37; _.56; _.73; 1]; r=[_.19; _.27; _.42; _.58; _.77; 1];
+  q=[_.23; _.29; _.48; _.71; 1]; r=[_.25; _.31; _.54; _.75; _.96; _.99 | _.100];
+  q=[_.17; _.21; _.37; _.56; _.73; _.90; 1]; r=[_.19; _.27; _.42; _.58; _.77; _.94; 1];
+  q=[_.23; _.29; _.48; _.71; _.92; 1]; r=[_.25; _.31; _.54; _.75; _.96; _.115; _.122 | _.123];
   }
   fun q -> lto (build_num 5) q, all answers {
-  q=[_.13; _.29; _.43; _.44 | _.45];
+  q=[_.13; _.23; _.39; _.44 | _.45];
   q=[0; 1; 1];
   q=[1; 1; 1];
   }
@@ -102,14 +102,14 @@
   fun q r s t -> divo q r s t, 6 answers {
   q=[]; r=[_.14 | _.15]; s=[]; t=[];
   q=[1]; r=[_.19; _.20 | _.21]; s=[]; t=[1];
-  q=[_.32; 1]; r=[_.34; _.63; _.64 | _.65]; s=[]; t=[_.32; 1];
-  q=[_.32; _.78; 1]; r=[_.34; _.80; _.117; _.118 | _.119]; s=[]; t=[_.32; _.78; 1];
-  q=[_.32; _.78; _.127; 1]; r=[_.34; _.80; _.129; _.174; _.175 | _.176]; s=[]; t=[_.32; _.78; _.127; 1];
-  q=[_.32; _.78; _.127; _.181; 1]; r=[_.34; _.80; _.129; _.183; _.216; _.217 | _.218]; s=[]; t=[_.32; _.78; _.127; _.181; 1];
+  q=[_.32; 1]; r=[_.34; _.50; _.64 | _.65]; s=[]; t=[_.32; 1];
+  q=[_.32; _.46; 1]; r=[_.34; _.50; _.98; _.118 | _.119]; s=[]; t=[_.32; _.46; 1];
+  q=[_.32; _.46; _.88; 1]; r=[_.34; _.50; _.98; _.157; _.175 | _.176]; s=[]; t=[_.32; _.46; _.88; 1];
+  q=[_.32; _.46; _.88; _.151; 1]; r=[_.34; _.50; _.98; _.157; _.201; _.217 | _.218]; s=[]; t=[_.32; _.46; _.88; _.151; 1];
   }
   fun q r s -> test27 q r s, 5 answers {
-  q=[]; r=[_.53; _.54 | _.55]; s=[0; 0; 1; 0; 0; 0; 1];
-  q=[1]; r=[_.1151; _.1152 | _.1153]; s=[1; 1; 0; 0; 0; 0; 1];
+  q=[]; r=[_.22; _.54 | _.55]; s=[0; 0; 1; 0; 0; 0; 1];
+  q=[1]; r=[_.16; _.1152 | _.1153]; s=[1; 1; 0; 0; 0; 0; 1];
   q=[0; 1]; r=[0; 1; 1]; s=[0; 0; 1];
   q=[1; 1]; r=[1; 1]; s=[1; 0; 0; 1; 0; 1];
   q=[0; 0; 1]; r=[1; 1]; s=[0; 0; 1];
diff --git a/regression/test017.t b/regression/test017.t
index 42811066..c7951372 100644
--- a/regression/test017.t
+++ b/regression/test017.t
@@ -64,24 +64,24 @@
   q=b;
   }
   fun q -> patho arco2 !!"a" q, 10 answers {
-  q=_.11;
+  q=_.10;
   q=a;
-  q=_.14;
-  q=_.15;
+  q=_.10;
+  q=_.10;
   q=a;
   q=a;
-  q=_.20;
-  q=_.21;
-  q=_.22;
-  q=_.23;
+  q=_.10;
+  q=_.10;
+  q=_.10;
+  q=_.10;
   }
   fun q -> patho_tabled !!"a" q, 10 answers {
-  q=_.11;
+  q=_.10;
   q=a;
   }
   fun q -> patho_tabled !!"a" q, 10 answers {
   q=a;
-  q=_.11;
+  q=_.10;
   }
   fun q -> patho arco3 !!"a" q, 10 answers {
   q=_.10 [=/= a; =/= b];
@@ -101,5 +101,5 @@
   }
   fun q -> patho_tabled !!"a" q, 10 answers {
   q=a;
-  q=_.11 [=/= a; =/= b];
+  q=_.10 [=/= a; =/= b];
   }
diff --git a/regression_ppx/test015.t b/regression_ppx/test015.t
index 3f690473..d182284e 100644
--- a/regression_ppx/test015.t
+++ b/regression_ppx/test015.t
@@ -3,9 +3,9 @@
   hd1 = _.12
   hd2 = _.14
   tl2 = _.15
-  10: { 0: [|  10 =/= _.11 |] }
+  11: { 0: [|  11 =/= _.10 |] }
   
-  11: { 0: [|  11 =/= boxed 0 <_.12, _.13> |] }
+  11: { 0: [|  11 =/= _.10 |] }
   
   15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
   
diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index b7a6da7c..892ded3b 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -153,7 +153,9 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       match walk env subst x, walk env subst y with
       | Var x, Var y ->
         if Term.Var.equal x y then acc
-        else extend x (Term.repr y) acc
+        else
+          let x, y = if not subsume && Term.Var.compare x y < 0 then y, x else x, y in
+          extend x (Term.repr y) acc
       | Var x, Value y -> extend x y acc
       | Value x, Var y -> extend y x acc
       | Value x, Value y  -> helper x y acc
diff --git a/src/core/Term.ml b/src/core/Term.ml
index 2d8ed6d6..55de726a 100644
--- a/src/core/Term.ml
+++ b/src/core/Term.ml
@@ -80,8 +80,7 @@ module Var =
 
     let reify r { index ; constraints } = index, List.map (fun x -> r @@ Obj.obj x) constraints
 
-    let equal x y =
-      (x.index = y.index) && (x.env = y.env)
+    let equal x y = x == y || x.index = y.index && x.env = y.env
 
     let compare x y =
       if x.index <> y.index then x.index - y.index else x.env - y.env