diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
index 56c5da967d..d63f5d4505 100644
--- a/pyk/src/pyk/k2lean4/k2lean4.py
+++ b/pyk/src/pyk/k2lean4/k2lean4.py
@@ -13,8 +13,10 @@
 from .model import (
     Alt,
     AltsFieldVal,
+    Axiom,
     Ctor,
     ExplBinder,
+    ImplBinder,
     Inductive,
     Instance,
     InstField,
@@ -207,6 +209,23 @@ def inj(subsort: str, supersort: str, x: str) -> Term:
 
         return res
 
+    def func_module(self) -> Module:
+        commands = [self._transform_func(func) for func in self.defn.functions]
+        return Module(commands=commands)
+
+    def _transform_func(self, func: str) -> Axiom:
+        ident = self._symbol_ident(func)
+        decl = self.defn.symbols[func]
+        sort_params = [var.name for var in decl.symbol.vars]
+        param_sorts = [sort.name for sort in decl.param_sorts]
+        sort = decl.sort.name
+
+        binders = []
+        if sort_params:
+            binders.append(ImplBinder(sort_params, Term('Type')))
+        binders.extend(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts))
+        return Axiom(ident, Signature(binders, Term(f'Option {sort}')))
+
 
 def _param_sorts(decl: SymbolDecl) -> list[str]:
     from ..utils import check_type