Bogus safety violation checking if a set is a subset of Nat. (#2971)

Keramelizer:
A \in SUBSET B  ~~>  \A a \in A: a \in B

Part of Github issue #2948
#2948

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala

@@ -105,6 +105,15 @@ class Keramelizer(gen: UniqueNameGenerator, tracker: TransformationTracker)
         .forall(tla.name(tempName).as(elemType), setX, tla.in(tla.name(tempName).as(elemType), setY).as(BoolT1))
         .as(BoolT1)
 
+    // rewrite A \in SUBSET B
+    // into \A a \in A: a \in B
+    case OperEx(TlaSetOper.in, setX, OperEx(TlaSetOper.powerset, setY)) =>
+      val elemType = getElemType(setX)
+      val tempName = gen.newName()
+      tla
+        .forall(tla.name(tempName).as(elemType), setX, tla.in(tla.name(tempName).as(elemType), setY).as(BoolT1))
+        .as(BoolT1)
+
     // rewrite f \in [S -> SUBSET T]
     // into DOMAIN f = S /\ \A x \in S: \A y \in f[x]: y \in T
     case OperEx(TlaSetOper.in, fun, OperEx(TlaSetOper.funSet, dom, OperEx(TlaSetOper.powerset, powSetDom))) =>

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestKeramelizer.scala

@@ -339,6 +339,26 @@ class TestKeramelizer extends AnyFunSuite with Checkers with BeforeAndAfterEach
     assert(expected == output)
   }
 
+  test("""A \in SUBSET B ~~> \A a \in A: a \in B""") {
+    val types = Map("BOOL" -> BoolT1, "POWSET" -> SetT1(SetT1(IntT1)), "SET" -> SetT1(IntT1), "INT" -> IntT1)
+    def A = tla.name("A") ? "SET"
+    def B = tla.name("B") ? "SET"
+    val input =
+      tla
+        .in(A, tla.powSet(B) ? "POWSET")
+        .typed(types, "BOOL")
+    val output = keramelizer.apply(input)
+
+    val isExpected = output match {
+      // \A element \in A: element \in B
+      case OperEx(TlaBoolOper.forall, NameEx(boundName), NameEx("A"),
+              OperEx(TlaSetOper.in, NameEx(inName), NameEx("B"))) =>
+        boundName == inName
+      case _ => false
+    }
+    assert(isExpected, s"Input $input and got $output")
+  }
+
   test("""A \subseteq B ~~> \A a \in A: a \in B""") {
     val types = Map("BOOL" -> BoolT1, "SET" -> SetT1(IntT1), "INT" -> IntT1)
     def A = tla.name("A") ? "SET"