diff --git a/src/pyk/proof/implies.py b/src/pyk/proof/implies.py
index da06329d5..945cc7c71 100644
--- a/src/pyk/proof/implies.py
+++ b/src/pyk/proof/implies.py
@@ -414,7 +414,7 @@ def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore):
         super().__init__(kcfg_explore)
         self.proof = proof
 
-    def step_proof(self, step: ImpliesProofStep) -> Iterable[ImpliesProofResult]:
+    def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]:
         proof_type = type(step.proof).__name__
         _LOGGER.info(f'Attempting {proof_type} {step.proof.id}')
 
diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py
index 684fd8868..dc632db68 100644
--- a/src/pyk/proof/reachability.py
+++ b/src/pyk/proof/reachability.py
@@ -138,7 +138,7 @@ def __init__(
                 assert type(subproof) is RefutationProof
                 self.node_refutations[node_id] = subproof
 
-    def get_steps(self) -> Iterable[APRProofStep]:
+    def get_steps(self) -> list[APRProofStep]:
         return [APRProofStep(self, node.id) for node in self.pending]
 
     def commit(self, result: APRProofResult) -> None:
@@ -724,7 +724,7 @@ def _check_subsume(self, node: KCFG.Node) -> CSubst | None:
             _LOGGER.info(f'Subsumed into target node {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}')
         return csubst
 
-    def step_proof(self, step: APRProofStep) -> Iterable[APRProofResult]:
+    def step_proof(self, step: APRProofStep) -> list[APRProofResult]:
         curr_node = step.proof.kcfg.node(step.node_id)
 
         if step.proof.bmc_depth is not None and curr_node.id not in self._checked_for_bounded:
@@ -754,7 +754,7 @@ def step_proof(self, step: APRProofStep) -> Iterable[APRProofResult]:
         is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(curr_node.cterm)
         target_is_terminal = step.proof.is_terminal(step.proof.target)
 
-        terminal_result = [APRProofTerminalResult(node_id=curr_node.id)] if is_terminal else []
+        terminal_result: list[APRProofResult] = [APRProofTerminalResult(node_id=curr_node.id)] if is_terminal else []
 
         # Subsumption should be checked if and only if the target node
         # and the current node are either both terminal or both not terminal