Theorem: Observational confluence

All liberal schedulers yield the same terminal observation law for a well-typed ${\mathsf{EC}}_{\mathrm{Born}}$ configuration.

Proof. The termination measure also decreases in liberal contexts. Induct on $m(t)$. If two first choices differ, refine each successor by firing the residual of the other redex. Lemma lem:diamond matches the resulting configurations with equal weights. The induction hypothesis identifies their terminal laws. If the first choices agree, apply induction to their successors.