diff --git a/k-files/imp-simple-spec.k b/k-files/imp-simple-spec.k
index 6e0dd4ccd7d..3a5cd90fdcd 100644
--- a/k-files/imp-simple-spec.k
+++ b/k-files/imp-simple-spec.k
@@ -9,8 +9,11 @@ module IMP-SIMPLE-SPEC
 
     claim [addition-var]: <k> 3 + N => 7 ... </k> requires N ==Int 4
 
+    claim [pre-branch-proved]: <k> $n = 7 ; if (B:Bool) { $n = 6 ; } else { $n = 5 ; } ~> #FINISH => if (B:Bool) { $n = 6 ; } else { $n = 5 ; } ~> #FINISH </k>
+                               <state> $n |-> (0 => 7) </state>
+
     claim [sum-10]: <k> int $s, $n, .Ids ; $n = 10 ; while (0 <= $n) { $s = $s + $n ; $n = $n + -1 ; } ~> #FINISH => . ... </k>
-                     <state> .Map => $s |-> 55 $n |-> -1 </state>
+                    <state> .Map => $s |-> 55 $n |-> -1 </state>
 
     claim [sum-100]: <k> int $s, $n, .Ids ; $n = 100 ; while (0 <= $n) { $s = $s + $n ; $n = $n + -1 ; } ~> #FINISH => . ... </k>
                      <state> .Map => $s |-> 5050 $n |-> -1 </state>
diff --git a/package/version b/package/version
index 5eb8803f31e..b1453c3a10c 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.225
+0.1.226
diff --git a/pyproject.toml b/pyproject.toml
index fe68e510e05..145666211bf 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.225"
+version = "0.1.226"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py
index f0cfd055171..a73440fbc51 100644
--- a/src/pyk/cterm.py
+++ b/src/pyk/cterm.py
@@ -17,6 +17,7 @@
     remove_generated_cells,
     simplify_bool,
     split_config_and_constraints,
+    split_config_from,
 )
 from .kast.outer import KClaim, KRule
 from .prelude.k import GENERATED_TOP_CELL
@@ -94,6 +95,14 @@ def kast(self) -> KInner:
     def hash(self) -> str:
         return self.kast.hash
 
+    @cached_property
+    def cells(self) -> Subst:
+        _, subst = split_config_from(self.config)
+        return Subst(subst)
+
+    def cell(self, cell: str) -> KInner:
+        return self.cells[cell]
+
     def match(self, cterm: CTerm) -> Subst | None:
         csubst = self.match_with_constraint(cterm)
 
diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py
index ad2c11e1cc7..7f638dcab06 100644
--- a/src/pyk/proof/reachability.py
+++ b/src/pyk/proof/reachability.py
@@ -70,6 +70,27 @@ class AGProver:
     def __init__(self, proof: AGProof) -> None:
         self.proof = proof
 
+    def _check_subsumption(
+        self,
+        kcfg_explore: KCFGExplore,
+        curr_node: KCFG.Node,
+        is_terminal: Callable[[CTerm], bool] | None = None,
+        implication_every_block: bool = True,
+    ) -> bool:
+        if implication_every_block or (is_terminal is not None and is_terminal(curr_node.cterm)):
+            target_node = self.proof.kcfg.get_unique_target()
+            _LOGGER.info(
+                f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
+            )
+            csubst = kcfg_explore.cterm_implies(curr_node.cterm, target_node.cterm)
+            if csubst is not None:
+                self.proof.kcfg.create_cover(curr_node.id, target_node.id, csubst=csubst)
+                _LOGGER.info(
+                    f'Subsumed into target node {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
+                )
+                return True
+        return False
+
     def advance_proof(
         self,
         kcfg_explore: KCFGExplore,
@@ -79,10 +100,8 @@ def advance_proof(
         execute_depth: int | None = None,
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
-        simplify_init: bool = True,
         implication_every_block: bool = True,
     ) -> KCFG:
-        target_node = self.proof.kcfg.get_unique_target()
         iterations = 0
 
         while self.proof.kcfg.frontier:
@@ -94,17 +113,10 @@ def advance_proof(
             iterations += 1
             curr_node = self.proof.kcfg.frontier[0]
 
-            if implication_every_block or (is_terminal is not None and is_terminal(curr_node.cterm)):
-                _LOGGER.info(
-                    f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
-                )
-                csubst = kcfg_explore.cterm_implies(curr_node.cterm, target_node.cterm)
-                if csubst is not None:
-                    self.proof.kcfg.create_cover(curr_node.id, target_node.id, csubst=csubst)
-                    _LOGGER.info(
-                        f'Subsumed into target node {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
-                    )
-                    continue
+            if self._check_subsumption(
+                kcfg_explore, curr_node, is_terminal=is_terminal, implication_every_block=implication_every_block
+            ):
+                continue
 
             if is_terminal is not None:
                 _LOGGER.info(f'Checking terminal {self.proof.id}: {shorten_hashes(curr_node.id)}')
@@ -132,6 +144,11 @@ def advance_proof(
                 )
                 curr_node = next_node
 
+                if self._check_subsumption(
+                    kcfg_explore, curr_node, is_terminal=is_terminal, implication_every_block=implication_every_block
+                ):
+                    continue
+
             if len(next_cterms) == 0:
                 _LOGGER.info(f'Found stuck node {self.proof.id}: {shorten_hashes(curr_node.id)}')
 
diff --git a/src/tests/integration/kcfg/test_cell_map.py b/src/tests/integration/kcfg/test_cell_map.py
index 0bb3976b114..77b3948999e 100644
--- a/src/tests/integration/kcfg/test_cell_map.py
+++ b/src/tests/integration/kcfg/test_cell_map.py
@@ -7,7 +7,6 @@
 
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KSequence, KToken, KVariable, build_assoc
-from pyk.kast.manip import get_cell
 from pyk.kcfg import KCFG
 from pyk.proof import AGProof, AGProver
 
@@ -103,7 +102,7 @@ def test_execute(
         actual_depth, actual_post_term, _ = kcfg_explore.cterm_execute(
             self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth
         )
-        actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'K_CELL'))
+        actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL'))
 
         # Then
         assert actual_depth == expected_depth
diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py
index 2c68526d64f..ee6f7c22c84 100644
--- a/src/tests/integration/kcfg/test_imp.py
+++ b/src/tests/integration/kcfg/test_imp.py
@@ -7,7 +7,6 @@
 
 from pyk.cterm import CSubst, CTerm
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
-from pyk.kast.manip import get_cell
 from pyk.kcfg import KCFG
 from pyk.prelude.kint import intToken
 from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue
@@ -111,6 +110,7 @@
     ('imp-simple-addition-1', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'addition-1', 2, 1, []),
     ('imp-simple-addition-2', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'addition-2', 2, 7, []),
     ('imp-simple-addition-var', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'addition-var', 2, 1, []),
+    ('pre-branch-proved', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'pre-branch-proved', 1, 100, []),
     (
         'imp-simple-sum-10',
         'k-files/imp-simple-spec.k',
@@ -193,13 +193,13 @@ def test_execute(
         actual_depth, actual_post_term, actual_next_terms = kcfg_explore.cterm_execute(
             self.config(kcfg_explore.kprint, k, state), depth=depth
         )
-        actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'K_CELL'))
-        actual_state = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'STATE_CELL'))
+        actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL'))
+        actual_state = kcfg_explore.kprint.pretty_print(actual_post_term.cell('STATE_CELL'))
 
         actual_next_states = [
             (
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'K_CELL')),
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'STATE_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('K_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')),
             )
             for s in actual_next_terms
         ]
diff --git a/src/tests/integration/kcfg/test_simple.py b/src/tests/integration/kcfg/test_simple.py
index 6312454d5f8..fb7fcbd481d 100644
--- a/src/tests/integration/kcfg/test_simple.py
+++ b/src/tests/integration/kcfg/test_simple.py
@@ -81,12 +81,12 @@ def test_execute(
         actual_depth, actual_post_term, actual_next_terms = kcfg_explore.cterm_execute(
             self.config(kcfg_explore.kprint, *pre), depth=depth
         )
-        actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'K_CELL'))
-        actual_state = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'STATE_CELL'))
+        actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL'))
+        actual_state = kcfg_explore.kprint.pretty_print(actual_post_term.cell('STATE_CELL'))
         actual_next_states = [
             (
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'K_CELL')),
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'STATE_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('K_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')),
             )
             for s in actual_next_terms
         ]
diff --git a/src/tests/integration/test_krun.py b/src/tests/integration/test_krun.py
index 3c0a799e946..d6c6081e983 100644
--- a/src/tests/integration/test_krun.py
+++ b/src/tests/integration/test_krun.py
@@ -5,7 +5,7 @@
 import pytest
 
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, Subst
-from pyk.kast.manip import flatten_label, get_cell
+from pyk.kast.manip import flatten_label
 from pyk.kore.prelude import int_dv
 from pyk.kore.syntax import App
 from pyk.prelude.kint import intToken
@@ -34,8 +34,8 @@ def test_run(self, krun: KRun) -> None:
         ]
 
         # When
-        actual_k = get_cell(final_cterm.config, 'K_CELL')
-        actual_map_items = flatten_label('_Map_', get_cell(final_cterm.config, 'STATE_CELL'))
+        actual_k = final_cterm.cell('K_CELL')
+        actual_map_items = flatten_label('_Map_', final_cterm.cell('STATE_CELL'))
 
         assert actual_k == expected_k
         assert set(actual_map_items) == set(expected_map_items)