diff --git a/src/MiniJuvix/Termination/Types/SizeRelation.hs b/src/MiniJuvix/Termination/Types/SizeRelation.hs
index f4309e8d1..8d3d37f14 100644
--- a/src/MiniJuvix/Termination/Types/SizeRelation.hs
+++ b/src/MiniJuvix/Termination/Types/SizeRelation.hs
@@ -61,5 +61,5 @@ instance Pretty Rel where
 
 instance Pretty Rel' where
   pretty r = case r of
-    REq -> pretty ("∼" :: Text)
+    REq -> pretty ("=" :: Text)
     RLe -> pretty ("≺" :: Text)
diff --git a/tests/positive/Termination/Data/List.mjuvix b/tests/positive/Termination/Data/List.mjuvix
index 6ef3c577a..ed0363f11 100644
--- a/tests/positive/Termination/Data/List.mjuvix
+++ b/tests/positive/Termination/Data/List.mjuvix
@@ -88,4 +88,19 @@ aux A (cons _ x xs) ls := cons A x (aux A xs ls);
 flat A (nil _)       := nil A;
 flat A (cons _ x xs) := aux A x xs;
 
+inductive Ord {
+  ZOrd : Ord;
+  SOrd : Ord -> Ord;
+  Lim  : (ℕ -> Ord) -> Ord;
+};
+
+addord : Ord -> Ord -> Ord;
+aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord);
+
+addord (Zord)   y := y;
+addord (SOrd x) y := SOrd (addord x y);
+addord (Lim f)  y := Lim (aux-addord f y);
+-- where
+aux-addord f y z := addord (f z) y;
+
 end;
\ No newline at end of file