diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
index f94fc00d..740942e6 100644
--- a/shared/src/main/scala/org/sireum/logika/Logika.scala
+++ b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -993,9 +993,9 @@ import Util._
         }
         return s0
       }
-      if (normPCs.contains(loHiCondExp)) {
+      if (normPCs.contains(th.normalizeExp(loHiCondExp))) {
         return accept(loHiCondExp.prettyST, "is in")
-      } else if (normPCs.contains(th.normalizeExp(loCondExp)) && normPCs.contains(hiCondExp)) {
+      } else if (normPCs.contains(th.normalizeExp(loCondExp)) && normPCs.contains(th.normalizeExp(hiCondExp))) {
         return accept(st"{ ${loCondExp.prettyST}; ${hiCondExp.prettyST} }", "is a subset of")
       } else {
         val sizeCond = hiCondExp.right