Generate binders for variables in definedness constraints (#4751)

This PR fixes a bug in the generator where a variable is not declared in
the signature of a `Rewrites` constructor if it only occurs in a
definedness constraint.

Author: tothtamas28

pyk/src/pyk/klean/k2lean4.py

@@ -326,7 +326,9 @@ def _rewrite_ctor(self, rule: RewriteRule) -> Ctor:
 
         # Step 3: create binders
         binders: list[Binder] = []
-        binders.extend(self._free_binders(pattern))  # Binders of the form {x y : SortInt}
+        binders.extend(
+            self._free_binders(And(SortApp('Foo'), (pattern,) + tuple(defs.values())))
+        )  # Binders of the form {x y : SortInt}
         binders.extend(self._def_binders(defs))  # Binders of the form (def_y : foo x = some y)
 
         # Step 4: transform patterns