diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
index 373aeb2d1d..df94fe0b2f 100644
--- a/pyk/src/pyk/k2lean4/k2lean4.py
+++ b/pyk/src/pyk/k2lean4/k2lean4.py
@@ -74,25 +74,24 @@ def ordering(sorts: list[str]) -> dict[str, list[str]]:
         sorts = list(TopologicalSorter(ordering(sorts)).static_order())
         return [self._cell(sort) for sort in sorts]
 
-    def _cell(self, sort: str) -> Structure:
+    def _cell(self, sort: str) -> Inductive | Structure:
         (cell_ctor,) = self.defn.constructors[sort]
         decl = self.defn.symbols[cell_ctor]
         param_sorts = _param_sorts(decl)
 
-        param_names: list[str]
-
-        if all(self._is_cell(sort) for sort in param_sorts):
-            param_names = []
-            for param_sort in param_sorts:
-                assert param_sort.startswith('Sort')
-                assert param_sort.endswith('Cell')
-                name = param_sort[4:-4]
-                name = name[0].lower() + name[1:]
-                param_names.append(name)
-        else:
+        if any(not self._is_cell(sort) for sort in param_sorts):
             assert len(param_sorts) == 1
-            param_names = ['val']
-
+            (param_sort,) = param_sorts
+            ctor = Ctor('mk', Signature((ExplBinder(('val',), Term(param_sort)),), Term(sort)))
+            return Inductive(sort, Signature((), Term('Type')), ctors=(ctor,))
+
+        param_names = []
+        for param_sort in param_sorts:
+            assert param_sort.startswith('Sort')
+            assert param_sort.endswith('Cell')
+            name = param_sort[4:-4]
+            name = name[0].lower() + name[1:]
+            param_names.append(name)
         fields = tuple(ExplBinder((name,), Term(sort)) for name, sort in zip(param_names, param_sorts, strict=True))
         return Structure(sort, Signature((), Term('Type')), ctor=StructCtor(fields))