For every grammar $𝐴$ and every term $𝜑:▷𝐴⊢𝐴$, where $▷$ is the later on grammars, there is a unique global parse $\text{𝗅ö𝖻}𝜑:\top ⊢𝐴$ with

Here $\text{𝗇𝖾𝗑𝗍}𝑡:\top ⊢▷𝐴$ restricts a global parse $𝑡$ to every proper suffix.

The proof is recursion on the length of the string. At $𝑣$, the parses already built at the proper suffixes of $𝑣$ form an element of $(▷𝐴)𝑣$, and $𝜑$ turns it into a parse at $𝑣$. Uniqueness is Löb for families over the proper-suffix order. In the Agda, lob in Grammar/Later/Base.agda is this recursion, done by well-founded induction on length.

To prove an entailment $𝐵⊢𝐶$ this way, apply Löb to $𝐴=𝐵\Rightarrow 𝐶$. The hypothesis $▷(𝐵\Rightarrow 𝐶)$ is the induction hypothesis at every proper suffix. It becomes usable once a non-nullable grammar has been consumed. If $𝜀\&𝐵⊢\perp$, then

because a parse of $𝐵\otimes \top$ over $𝑣$ splits $𝑣=𝑥\text{++}𝑢$ with $𝑥$ non-empty, so $𝑢⊏𝑣$. This is ▷-app-NE in Grammar/Later/Properties.agda. Induction on a Kleene star is the standard use.